;;;===========================================================================
;;;
;;; Cone Equivalence Theorem (Second Version)
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 26/05/10 || End date: 27/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "cone2-structure")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-Z *) => *)
 ;; Addition operation ring
 ((addition-ring-Z * *)=> *)
 ;; Product operation ring
 ((product-ring-Z * *) => *)
 ;; Inverse ring
 ((inverse-Z *) => *)
 ;; Zero element ring
 ((zero-element-Z ) => *)
 ;; Unit element ring
 ((unit-Z )=> *)

 ;;--------------------------------------------------
 ;; First homotopy equivalence C1 <<= D1 =>> H1
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C1 * *) => *)
 ;; Group Operation 
 ((group-operation-C1 * * *) => *)
 ;; Zero element
 ((zero-C1 *) => *)
 ;; External multiplication
 ((external-C1 * * *) => *)
 ;; Inverse element
 ((inverse-C1 * *) => *)

 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C1 * *) => *)

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D1 * *) => *)
 ;; Group Operation 
 ((group-operation-D1 * * *) => *)
 ;; Zero element
 ((zero-D1 *) => *)
 ;; External multiplication
 ((external-D1 * * *) => *)
 ;; Inverse element
 ((inverse-D1 * *) => *)

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D1 * *) => *)

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-H1 * *) => *)
 ;; Group Operation 
 ((group-operation-H1 * * *) => *)
 ;; Zero element
 ((zero-H1 *) => *)
 ;; External multiplication
 ((external-H1 * * *) => *)
 ;; Inverse element
 ((inverse-H1 * *) => *)

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-H1 * *) => *)

 ;;--------------------------------------------------
 ;; Second homotopy equivalence C2 <<= D2 =>> H2
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; C2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C2 * *) => *)
 ;; Group Operation 
 ((group-operation-C2 * * *) => *)
 ;; Zero element
 ((zero-C2 *) => *)
 ;; External multiplication
 ((external-C2 * * *) => *)
 ;; Inverse element
 ((inverse-C2 * *) => *)

 ;;--------------------------------------------------
 ;; The C2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C2 * *) => *)

 ;;--------------------------------------------------
 ;; D2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D2 * *) => *)
 ;; Group Operation 
 ((group-operation-D2 * * *) => *)
 ;; Zero element
 ((zero-D2 *) => *)
 ;; External multiplication
 ((external-D2 * * *) => *)
 ;; Inverse element
 ((inverse-D2 * *) => *)

 ;;--------------------------------------------------
 ;; The D2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D2 * *) => *)

  ;;--------------------------------------------------
 ;; H2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-H2 * *) => *)
 ;; Group Operation 
 ((group-operation-H2 * * *) => *)
 ;; Zero element
 ((zero-H2 *) => *)
 ;; External multiplication
 ((external-H2 * * *) => *)
 ;; Inverse element
 ((inverse-H2 * *) => *)

 ;;--------------------------------------------------
 ;; The H2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-H2 * *) => *)

 
 ;;--------------------------------------------------
 ;; Morphisms of the first homotopy equivalence
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lf1 * *) => *)

 ;;--------------------------------------------------
 ;; The lg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lg1 * *) => *)


 ;;--------------------------------------------------
 ;; The lh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lh1 * *) => *)

 ;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rf1 * *) => *)

 ;;--------------------------------------------------
 ;; The rg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rg1 * *) => *)


 ;;--------------------------------------------------
 ;; The rh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rh1 * *) => *)

 ;;--------------------------------------------------
 ;; The lf2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lf2 * *) => *)

 ;;--------------------------------------------------
 ;; The lg2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lg2 * *) => *)


 ;;--------------------------------------------------
 ;; The lh2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lh2 * *) => *)

 ;;--------------------------------------------------
 ;; The rf2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rf2 * *) => *)

 ;;--------------------------------------------------
 ;; The rg2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rg2 * *) => *)


 ;;--------------------------------------------------
 ;; The rh2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rh2 * *) => *)


 ;;--------------------------------------------------
 ;; The morphism phi-c2-c1: C2 -> C1
 ;;--------------------------------------------------

 ;; The function
 ((phi-c2-c1 * *) => *)
 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-Z (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-Z (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring-Z (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-Z (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element-Z nil
	  0))

 ;; Unit element ring
 (local (defun unit-Z nil
	  1))

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D1 (n a)
	  (declare (ignore n a))
	  0))

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-H1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-H1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-H1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-H1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-H1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-H1 (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; C2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; D2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The D2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D2 (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; H2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-H2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-H2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-H2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-H2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-H2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The H2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-H2 (n a)
	  (declare (ignore n a))
	  0))
 


 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lh1 (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rh1 (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; The lf2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lf2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lg2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lg2 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lh2 (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rf2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rf2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rg2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rg2 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rh2 (n a)
	  (declare (ignore n a))
	  0))


 

 ;;--------------------------------------------------
 ;; The morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun phi-c2-c1 (n a)
	  (declare (ignore n a))
	  0))


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-C1 'group-operation-C1 'zero-C1 'external-C1 'inverse-C1 'd-C1 )
  'lf1  'lg1  'lh1
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-H1 'group-operation-H1 'zero-H1 'external-H1 'inverse-H1 'd-H1 )
  'rf1  'rg1  'rh1
  ))
 'homotopy-equivalence-1
   )


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D2 'group-operation-D2 'zero-D2 'external-D2 'inverse-D2 'd-D2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-C2 'group-operation-C2 'zero-C2 'external-C2 'inverse-C2 'd-C2 )
  'lf2  'lg2  'lh2
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D2 'group-operation-D2 'zero-D2 'external-D2 'inverse-D2 'd-D2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-H2 'group-operation-H2 'zero-H2 'external-H2 'inverse-H2 'd-H2 )
  'rf2  'rg2  'rh2
  ))
 'homotopy-equivalence-2
   )


(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 'inv-C2 'group-operation-C2 'zero-C2 'external-C2 'inverse-C2 'd-C2 )
 (chain-complex 'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 'inv-C1 'group-operation-C1 'zero-C1 'external-C1 'inverse-C1 'd-C1 )
 'phi-c2-c1) 'phi-c2-c1)

)


)


;;==================================================
;; The Cone definitions
;;==================================================

;;--------------------------------------------------
;; Cone from phi: C2 -> C1
;;--------------------------------------------------

(encapsulate 

 ()
 
(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C2 group-operation-C2 zero-C2 external-C2 inverse-C2 d-C2 C2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|))))))

(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C1 group-operation-C1 zero-C1 external-C1 inverse-C1 d-C1 C1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|))))))

(in-theory (disable COMMUTATIVITY-OF-+))

(local (defthm help1 (IMPLIES (AND (INV-C2 N A)
              (INV-C2 N B)
              (INV-C2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C2 N (GROUP-OPERATION-C2 N A B) C)
                (GROUP-OPERATION-C2 N A (GROUP-OPERATION-C2 N B C)))) 
:hints (("Goal" :use ((:instance |C2-is-a-chain-complex|))))))

(local (defthm help3 (IMPLIES (AND (INV-C1 N A)
              (INV-C1 N B)
              (INV-C1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C1 N (GROUP-OPERATION-C1 N A B) C)
                (GROUP-OPERATION-C1 N A (GROUP-OPERATION-C1 N B C)))) 
:hints (("Goal" :use ((:instance |C1-is-a-chain-complex|))))))

(definstance-*cone2*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-C2)
    (group-operation-D group-operation-C2)
    (zero-D zero-C2)
    (external-D external-C2)
    (inverse-D inverse-C2)
    (d-D d-C2)
    (inv-C inv-C1) 
    (group-operation-C group-operation-C1)
    (zero-C zero-C1)
    (external-C external-C1)
    (inverse-C inverse-C1)
    (d-C d-C1)    
    (phi phi-c2-c1))
  "-cone-C2-C1")
)


;;--------------------------------------------------
;; Cone from dphi: D2 -> D1
;;--------------------------------------------------

(defun phi-d2-d1 (n a)
  (lg1 n (phi-c2-c1 n (lf2 n a))))

(encapsulate 

 ()

(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D2 group-operation-D2 zero-D2 external-D2 inverse-D2 d-D2 D2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|))))))

(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D1 group-operation-D1 zero-D1 external-D1 inverse-D1 d-D1 D1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|))))))

(local (defthm help1 (IMPLIES (AND (INV-D2 N A)
              (INV-D2 N B)
              (INV-D2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D2 N (GROUP-OPERATION-D2 N A B) C)
                (GROUP-OPERATION-D2 N A (GROUP-OPERATION-D2 N B C)))) 
:hints (("Goal" :use ((:instance |D2-is-a-chain-complex|))))))

(local (defthm help3 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N (GROUP-OPERATION-D1 N A B) C)
                (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C)))) 
:hints (("Goal" :use ((:instance |D1-is-a-chain-complex|))))))



(definstance-*cone2*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-D2)
    (group-operation-D group-operation-D2)
    (zero-D zero-D2)
    (external-D external-D2)
    (inverse-D inverse-D2)
    (d-D d-D2)
    (inv-C inv-D1) 
    (group-operation-C group-operation-D1)
    (zero-C zero-D1)
    (external-C external-D1)
    (inverse-C inverse-D1)
    (d-C d-D1)    
    (phi phi-d2-d1))
  "-cone-D2-D1")

)

;;--------------------------------------------------
;; Cone from hphi: H2 -> H1
;;--------------------------------------------------


(defun phi-h2-h1 (n a)
  (rf1 n (phi-d2-d1 n (rg2 n a))))


(encapsulate 

 ()

(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H2 group-operation-H2 zero-H2 external-H2 inverse-H2 d-H2 H2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|))))))

(local (defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H1 group-operation-H1 zero-H1 external-H1 inverse-H1 d-H1 H1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|))))))

(local (defthm help1 (IMPLIES (AND (INV-H2 N A)
              (INV-H2 N B)
              (INV-H2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H2 N (GROUP-OPERATION-H2 N A B) C)
                (GROUP-OPERATION-H2 N A (GROUP-OPERATION-H2 N B C)))) 
:hints (("Goal" :use ((:instance |H2-is-a-chain-complex|))))))

(local (defthm help3 (IMPLIES (AND (INV-H1 N A)
              (INV-H1 N B)
              (INV-H1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H1 N (GROUP-OPERATION-H1 N A B) C)
                (GROUP-OPERATION-H1 N A (GROUP-OPERATION-H1 N B C)))) 
:hints (("Goal" :use ((:instance |H1-is-a-chain-complex|))))))



(definstance-*cone2*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-H2)
    (group-operation-D group-operation-H2)
    (zero-D zero-H2)
    (external-D external-H2)
    (inverse-D inverse-H2)
    (d-D d-H2)
    (inv-C inv-H1) 
    (group-operation-C group-operation-H1)
    (zero-C zero-H1)
    (external-C external-H1)
    (inverse-C inverse-H1)
    (d-C d-H1)    
    (phi phi-h2-h1))
  "-cone-H2-H1")
)

;;;--------------------------------------------------
;;; Morphisms of the equivalence
;;;--------------------------------------------------

(defun lf-cones (n a)
  (list (lf1 (1+ n) (car a))
	(lf2 n (cadr a))))

(defun lg-cones (n a)
  (list (lg1 (1+ n) (car a))
	(lg2 n (cadr a))))

(defun lh-cones (n a)
  (list (lh1 (1+ n) (car a))
	(inverse-D2 (1+ n) (lh2 n (cadr a)))))

(defun rf-cones (n a)
  (list (group-operation-H1 (1+ n) (rf1 (1+ n) (car a))
			    (rf1 (1+ n) (phi-d2-d1 (1+ n) (rh2 n (cadr a)))))
	(rf2 n (cadr a))))

(defun rg-cones (n a)
  (list
   (group-operation-D1 (1+ n) (rg1 (1+ n) (car a))
		       (inverse-D1 (1+ n) (rh1 n (phi-d2-d1 n (rg2 n (cadr a))))))
   (rg2 n (cadr a))))

(defun rh-cones (n a)
  (list
   (group-operation-D1 (1+ (1+ n)) (rh1 (1+ n) (car a))
		       (rh1 (1+ n) (phi-d2-d1 (1+ n) (rh2 n (cadr a)))))
   (inverse-D2 (1+ n) (rh2 n (cadr a)))
   ))


;;;--------------------------------------------------
;;; Auxiliar Theorems
;;;--------------------------------------------------


(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-cone-cone-d2-d1 group-operation-cone-cone-d2-d1 zero-cone-cone-d2-d1 external-cone-cone-d2-d1 inverse-cone-cone-d2-d1 d-cone-cone-d2-d1 cone-d2-d1
	 :hints (("Goal" :use ((:instance |CONE2-D-CHI-C-is-a-chain-complex-CONE-D2-D1| )))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H1 group-operation-H1 zero-H1 external-H1 inverse-H1 d-H1 H1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))



(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D2 group-operation-D2 zero-D2 external-D2 inverse-D2 d-D2 D2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))


(defthm help1 (IMPLIES (AND (INV-D2 N A)
              (INV-D2 N B)
              (INV-D2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D2 N (GROUP-OPERATION-D2 N A B) C)
                (GROUP-OPERATION-D2 N A (GROUP-OPERATION-D2 N B C)))) 
:hints (("Goal" :use ((:instance |D2-is-a-chain-complex|)))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D1 group-operation-D1 zero-D1 external-D1 inverse-D1 d-D1 D1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))
 
(defthm help3 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N (GROUP-OPERATION-D1 N A B) C)
                (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C)))) 
:hints (("Goal" :use ((:instance |D1-is-a-chain-complex|)))))



(in-theory (disable |D1-is-a-chain-complex|
		    |D2-is-a-chain-complex|
		    |CONE2-D-CHI-C-is-a-chain-complex-CONE-D2-D1|))


(defthm group-operation-d1-commutativity
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(integerp n))
	   (equal (group-operation-d1 n a b)
		  (group-operation-d1 n b a))))
	   

(defthm help3-bis (IMPLIES (AND (INV-D1 (+ 1 N) A)
              (INV-D1 (+ 1 N) B)
              (INV-D1 (+ 1 N) C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 (+ 1 N) A (GROUP-OPERATION-D1 (+ 1 N) B C))
		(GROUP-OPERATION-D1 (+ 1 N) c (GROUP-OPERATION-D1 (+ 1 N) A B))
                )) 
:hints (("Goal" :use ((:instance help3 (n (+ 1 N)))))))



(defthm group-operation-d2-commutativity
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(integerp n))
	   (equal (group-operation-d2 n a b)
		  (group-operation-d2 n b a))))
	   

(defthm help1-bis (IMPLIES (AND (INV-D2 n A)
              (INV-D2 n B)
              (INV-D2 n C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D2 n A (GROUP-OPERATION-D2 n B C))
		(GROUP-OPERATION-D2 n c (GROUP-OPERATION-D2 n A B))
                )) 
:hints (("Goal" :use ((:instance help1)))))

(defthm inv-d-d1
  (implies (and (inv-d1 n a) (integerp n))
	   (inv-d1 (+ n -1) (d-d1 n a)))
   :hints (("Goal" 
	   :use ((:instance |D1-is-a-chain-complex|)))))

(defthm -1+1+n=n
	 (implies (integerp n)
		  (equal (1- (+ 1 n)) n))
	 :rule-classes nil)

(defthm +1+n-1=n
	 (implies (integerp n)
		  (equal (+ (+ 1 n) -1) n))
	 :rule-classes nil)

(defthm inv-d-d1-2
  (implies (and (inv-d1 (+ 1 n) a) (integerp n))
	   (inv-d1 (+ (+ 1 n) -1) (d-d1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-d1
			    (n (+ 1 n))
			    )
		 ))))


(defthm inv-d-d1-3
  (implies (and (inv-d1 (+ 1 n) a) (integerp n))
	   (inv-d1 n (d-d1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance +1+n-1=n)
		 (:instance inv-d-d1-2)
		 ))))


(defthm inv-d-d1-lg1-phi-lf2
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d1 n (LG1 N (PHI-C2-C1 N (LF2 N A))))))


(defthm inv-d1-+1+n-1
  (implies (integerp n)
	   (equal (inv-d1 (+ 1 N -1) a)
		  (inv-d1 n a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm inv-d2-inverse
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ n -1) (INVERSE-D2 (+ N -1) (D-D2 N a)))))
  
(defthm +n-1=-1+n
  (equal (+ n -1) (+ -1 n))
  :rule-classes nil)


(defthm inv-d2-inverse-bis
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ n -1) (INVERSE-D2 (+ -1 n) (D-D2 N a))))
  :hints (("Goal" :use ((:instance +n-1=-1+n)
			(:instance inv-d2-inverse)))))
		
(defthm group-operation-d1-d1-+1+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-D1 (+ 1 N -1) a b)
		  (GROUP-OPERATION-D1 n a b)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))

(DEFTHM
  HELP3-BIS2
  (IMPLIES
   (AND (INV-D1 n A)
	(INV-D1 n B)
	(INV-D1 n C)
	(INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D1 n
			A (GROUP-OPERATION-D1 n B C))
    (GROUP-OPERATION-D1 n
			C (GROUP-OPERATION-D1 n A B))))
  :HINTS (("Goal" :USE ((:INSTANCE HELP3)))))


(defthm group-operation-d1-distrivutivity
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(integerp n))
	   (equal (group-operation-d1 n a (group-operation-d1 n b c))
		  (group-operation-d1 n b (group-operation-d1 n a c))))
  :hints (("Goal" :use ((:instance group-operation-d1-commutativity (a b) (b c))
			(:instance HELP3-BIS2 (a a) (b c) (c b)))))))



(defthm inv-d-d2
  (implies (and (inv-d2 n a) (integerp n))
	   (inv-d2 (+ n -1) (d-d2 n a)))
   :hints (("Goal" 
	   :use ((:instance |D2-is-a-chain-complex|)))))

(defthm group-operation-inverse-d2
  (implies (and (inv-d2 (+ n -1) a)
		(inv-d2 (+ n -1) b)
		(integerp n))
	   (equal (INVERSE-D2 (+ -1 N)
                   (GROUP-OPERATION-D2 (+ N -1) a b))
		  (GROUP-OPERATION-D2 (+ N -1)
                           (INVERSE-D2 (+ -1 N) a)
                           (INVERSE-D2 (+ -1 N) b))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))
     


(defthm external-d1-d1-+1+n-1
  (implies (and (integerp n)
		(inv-ring-z r))
	   (equal (EXTERNAL-D1 (+ 1 N -1) r a)
		  (EXTERNAL-D1 n r a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))

(defthm inverse-external-d2
  (implies (and (inv-d2 (+ n -1) a)
		(inv-ring-z r)
		(integerp n))
	   (equal (INVERSE-D2 (+ -1 N)
                   (external-D2 (+ N -1) r a))
		  (external-d2 (+ N -1) r (inverse-d2 (+ -1 N) a))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))
    

                           
(defthm zero-d1+1+n-1
  (implies (integerp n)
	   (equal (ZERO-D1 (+ 1 N -1)) (ZERO-D1 N)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))

(defthm inverse-zero-d2
  (implies (integerp n)
	   (EQUAL (INVERSE-D2 (+ -1 N) (ZERO-D2 (+ N -1)))
		  (ZERO-D2 (+ N -1))))
   :hints (("Goal" :use (:instance |+N-1=-1+N|))))
  

(defthm group-operation-inverse-d1
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(integerp n))
	   (equal (INVERSE-D1 (+ 1 N -1)
                   (GROUP-OPERATION-D1 n a b))
		  (GROUP-OPERATION-D1 n
                           (INVERSE-D1 (+ 1 N -1)  a)
                           (INVERSE-D1 n b))))
  :hints (("Goal" :use (:instance  +1+n-1=n))))


(defthm inverse-inverse-d2
  (implies (and (inv-d2 (+ n -1) a)
		(integerp n))
	   (EQUAL (INVERSE-D2 (+ -1 N)
			      (INVERSE-D2 (+ N -1) a))
		  (INVERSE-D2 (+ N -1)
			      (INVERSE-D2 (+ -1 N)
					  a))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm group-operation-c1-commutativity
  (implies (and (inv-c1 n a)
		(inv-c1 n b)
		(integerp n))
	   (equal (group-operation-c1 n a b)
		  (group-operation-c1 n b a)))
  )

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C1 group-operation-C1 zero-C1 external-C1 inverse-C1 d-C1 C1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))

(defthm group-operation-c1-distrivutivity
  (implies (and (inv-c1 n a)
		(inv-c1 n b)
		(inv-c1 n c)
		(integerp n))
	   (equal (group-operation-c1 n c (group-operation-c1 n a b))
		  (group-operation-c1 n a (group-operation-c1 n b c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |C1-is-a-chain-complex|)))))

(defthm group-operation-c1-distrivutivity-2
  (implies (and (inv-c1 n a)
		(inv-c1 n b)
		(inv-c1 n c)
		(integerp n))
	   (equal (group-operation-c1 n a (group-operation-c1 n b c))
		  (group-operation-c1 n b (group-operation-c1 n a c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-c1-commutativity
			    (a b) (b c))
		 (:instance group-operation-c1-distrivutivity
			    (c b) (b c))))))



(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C2 group-operation-C2 zero-C2 external-C2 inverse-C2 d-C2 C2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))


(defthm group-operation-c2-commutativity
  (implies (and (inv-c2 n a)
		(inv-c2 n b)
		(integerp n))
	   (equal (group-operation-c2 n a b)
		  (group-operation-c2 n b a)))
  )

(defthm group-operation-c2-distrivutivity
  (implies (and (inv-c2 n a)
		(inv-c2 n b)
		(inv-c2 n c)
		(integerp n))
	   (equal (group-operation-c2 n c (group-operation-c2 n a b))
		  (group-operation-c2 n a (group-operation-c2 n b c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |C2-is-a-chain-complex|)))))

(defthm group-operation-c2-distrivutivity-2
  (implies (and (inv-c2 n a)
		(inv-c2 n b)
		(inv-c2 n c)
		(integerp n))
	   (equal (group-operation-c2 n a (group-operation-c2 n b c))
		  (group-operation-c2 n b (group-operation-c2 n a c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-c2-commutativity
			    (a b) (b c))
		 (:instance group-operation-c2-distrivutivity
			    (c b) (b c))))))


(in-theory (disable |C1-is-a-chain-complex|
		    |C2-is-a-chain-complex|
		    group-operation-D1-commutativity
		    group-operation-c1-commutativity
		    group-operation-c2-commutativity))


(defthm inv-c1+1+n-1
  (implies (integerp n)
	   (equal (inv-c1 (+ 1 N -1) a) (inv-c1 N a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))



(defthm inv-d-c1
  (implies (and (inv-c1 n a) (integerp n))
	   (inv-c1 (+ n -1) (d-c1 n a)))
   :hints (("Goal" 
	   :use ((:instance |C1-is-a-chain-complex|)))))

(defthm inv-d-c1-2
  (implies (and (inv-c1 (+ 1 n) a) (integerp n))
	   (inv-c1 (+ (+ 1 n) -1) (d-c1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-c1
			    (n (+ 1 n))
			    )
		 ))))


(defthm inv-d-c1-3
  (implies (and (inv-c1 (+ 1 n) a) (integerp n))
	   (inv-c1 n (d-c1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance +1+n-1=n)
		 (:instance inv-d-c1-2)
		 ))))


(defthm inv-d-c2
  (implies (and (inv-c2 n a) (integerp n))
	   (inv-c2 (+ n -1) (d-c2 n a)))
   :hints (("Goal" 
	   :use ((:instance |C2-is-a-chain-complex|)))))


(defthm inverse-c2+n-1
  (implies (integerp n)
	   (equal (inverse-c2 (+ -1 n) a)
		  (inverse-c2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm group-operation-c1-c1-+1+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-c1 (+ 1 N -1) a b)
		  (GROUP-OPERATION-c1 n a b)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm external-c1-c1-+1+n-1
  (implies (and (integerp n)
		(inv-ring-z r))
	   (equal (EXTERNAL-c1 (+ 1 N -1) r a)
		  (EXTERNAL-c1 n r a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm zero-c1+1+n-1
  (implies (integerp n)
	   (equal (ZERO-c1 (+ 1 N -1)) (ZERO-c1 N)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))

(defthm group-operation-inverse-c1
  (implies (and (inv-c1 n a)
		(inv-c1 n b)
		(integerp n))
	   (equal (INVERSE-c1 (+ 1 N -1)
                   (GROUP-OPERATION-c1 n a b))
		  (GROUP-OPERATION-c1 n
                           (INVERSE-c1 (+ 1 N -1)  a)
                           (INVERSE-c1 n b))))
  :hints (("Goal" :use (:instance  +1+n-1=n))))

(defthm inverse-c1+1+n-1
  (implies (integerp n)
	   (equal (inverse-c1 (+ 1 N -1) a)
		  (inverse-c1 n a)))
  :hints (("Goal" :use (:instance  +1+n-1=n))))


(defthm group-operation-h1-commutativity
  (implies (and (inv-h1 n a)
		(inv-h1 n b)
		(integerp n))
	   (equal (group-operation-h1 n a b)
		  (group-operation-h1 n b a)))
  )

(defthm group-operation-h1-distrivutivity
  (implies (and (inv-h1 n a)
		(inv-h1 n b)
		(inv-h1 n c)
		(integerp n))
	   (equal (group-operation-h1 n c (group-operation-h1 n a b))
		  (group-operation-h1 n a (group-operation-h1 n b c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |H1-is-a-chain-complex|)))))

(defthm group-operation-h1-distrivutivity-2
  (implies (and (inv-h1 n a)
		(inv-h1 n b)
		(inv-h1 n c)
		(integerp n))
	   (equal (group-operation-h1 n a (group-operation-h1 n b c))
		  (group-operation-h1 n b (group-operation-h1 n a c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-h1-commutativity
			    (a b) (b c))
		 (:instance group-operation-h1-distrivutivity
			    (c b) (b c))))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H2 group-operation-H2 zero-H2 external-H2 inverse-H2 d-H2 H2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))


(defthm group-operation-h2-commutativity
  (implies (and (inv-h2 n a)
		(inv-h2 n b)
		(integerp n))
	   (equal (group-operation-h2 n a b)
		  (group-operation-h2 n b a)))
  )

(defthm group-operation-h2-distrivutivity
  (implies (and (inv-h2 n a)
		(inv-h2 n b)
		(inv-h2 n c)
		(integerp n))
	   (equal (group-operation-h2 n c (group-operation-h2 n a b))
		  (group-operation-h2 n a (group-operation-h2 n b c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |H2-is-a-chain-complex|)))))

(defthm group-operation-h2-distrivutivity-2
  (implies (and (inv-h2 n a)
		(inv-h2 n b)
		(inv-h2 n c)
		(integerp n))
	   (equal (group-operation-h2 n a (group-operation-h2 n b c))
		  (group-operation-h2 n b (group-operation-h2 n a c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-h2-commutativity
			    (a b) (b c))
		 (:instance group-operation-h2-distrivutivity
			    (c b) (b c))))))


(in-theory (disable |H1-is-a-chain-complex|
		    |H2-is-a-chain-complex|
		    group-operation-D1-commutativity
		    group-operation-h1-commutativity
		    group-operation-h2-commutativity))


(defthm inv-h1+1+n-1
  (implies (integerp n)
	   (equal (inv-h1 (+ 1 N -1) a) (inv-h1 N a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))



(defthm inv-d-h1
  (implies (and (inv-h1 n a) (integerp n))
	   (inv-h1 (+ n -1) (d-h1 n a)))
   :hints (("Goal" 
	   :use ((:instance |H1-is-a-chain-complex|)))))

(defthm inv-d-h1-2
  (implies (and (inv-h1 (+ 1 n) a) (integerp n))
	   (inv-h1 (+ (+ 1 n) -1) (d-h1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-h1
			    (n (+ 1 n))
			    )
		 ))))


(defthm inv-d-h1-3
  (implies (and (inv-h1 (+ 1 n) a) (integerp n))
	   (inv-h1 n (d-h1 (+ 1 n) a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance +1+n-1=n)
		 (:instance inv-d-h1-2)
		 ))))


(defthm inv-d-h2
  (implies (and (inv-h2 n a) (integerp n))
	   (inv-h2 (+ n -1) (d-h2 n a)))
   :hints (("Goal" 
	   :use ((:instance |H2-is-a-chain-complex|)))))


(defthm inverse-h2+n-1
  (implies (integerp n)
	   (equal (inverse-h2 (+ -1 n) a)
		  (inverse-h2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm group-operation-h1-h1-+1+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-h1 (+ 1 N -1) a b)
		  (GROUP-OPERATION-h1 n a b)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm external-h1-h1-+1+n-1
  (implies (and (integerp n)
		(inv-ring-z r))
	   (equal (EXTERNAL-h1 (+ 1 N -1) r a)
		  (EXTERNAL-h1 n r a)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm zero-h1+1+n-1
  (implies (integerp n)
	   (equal (ZERO-h1 (+ 1 N -1)) (ZERO-h1 N)))
  :hints (("Goal" 
	   :use (:instance +1+n-1=n))))


(defthm group-operation-inverse-h1
  (implies (and (inv-h1 n a)
		(inv-h1 n b)
		(integerp n))
	   (equal (INVERSE-h1 (+ 1 N -1)
                   (GROUP-OPERATION-h1 n a b))
		  (GROUP-OPERATION-h1 n
                           (INVERSE-h1 (+ 1 N -1)  a)
                           (INVERSE-h1 n b))))
  :hints (("Goal" :use (:instance  +1+n-1=n))))

(defthm inverse-h1+1+n-1
  (implies (integerp n)
	   (equal (inverse-h1 (+ 1 N -1) a)
		  (inverse-h1 n a)))
  :hints (("Goal" :use (:instance  +1+n-1=n))))



(DEFTHM
  INV-D-D2+n-2
  (IMPLIES (AND (INV-D2 (+ N -1) A) (INTEGERP N))
	   (INV-D2 (+ N -2) (D-D2 (+ N -1) A)))
  :HINTS (("Goal" :USE ((:INSTANCE INV-D-D2 (n (+ N -1)))))))

(defthm inverse-d2-1+n
  (implies (integerp n)
	   (equal (inverse-d2 (+ -1 n) a)
		  (inverse-d2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm d-d2-1+n
   (implies (integerp n)
	   (equal (d-d2 (+ -1 n) a)
		  (d-d2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm +n-2=-1-1+n
  (implies (integerp n)
	   (equal (+ -1 -1 N)
		  (+ N -2)))
  :rule-classes nil)


(defthm inverse-inverse-+n-2
  (implies (and (inv-d2 (+ n -2) a)
		(integerp n))
	   (equal (inverse-d2 (+ n -2) (inverse-d2 (+ n -2) a))
		  a)))


(defthm zero-d2-1-1+n
  (implies (integerp n)
	   (equal (ZERO-D2 (+ -1 -1 N))
		  (ZERO-D2 (+ N -2))))
  :hints (("Goal" :use (:instance +n-2=-1-1+n))))

(DEFTHM |-1+n=+N-1| (EQUAL (+ -1 n) (+ N -1))
                     :RULE-CLASSES NIL)


(defthm d-d2od-d2
  (implies (and (inv-d2 n a)
		(integerp n))
	   (EQUAL (D-D2 (+ N -1) (D-D2 N a))
		  (ZERO-D2 (+ -1 -1 N))))
  :hints (("Goal" :in-theory (disable d-d2-1+n)
	   :use (:instance |+N-1=-1+N|))))



(DEFTHM
  INV-D-c2+n-2
  (IMPLIES (AND (INV-c2 (+ N -1) A) (INTEGERP N))
	   (INV-c2 (+ N -2) (D-c2 (+ N -1) A)))
  :HINTS (("Goal" :USE ((:INSTANCE INV-D-c2 (n (+ N -1)))))))

(defthm inverse-c2-1+n
  (implies (integerp n)
	   (equal (inverse-c2 (+ -1 n) a)
		  (inverse-c2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm d-c2-1+n
   (implies (integerp n)
	   (equal (d-c2 (+ -1 n) a)
		  (d-c2 (+ n -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm inverse-inverse-c2-+n-2
  (implies (and (inv-c2 (+ n -2) a)
		(integerp n))
	   (equal (inverse-c2 (+ n -2) (inverse-c2 (+ n -2) a))
		  a)))


(defthm zero-c2-1-1+n
  (implies (integerp n)
	   (equal (ZERO-C2 (+ -1 -1 N))
		  (ZERO-C2 (+ N -2))))
  :hints (("Goal" :use (:instance +n-2=-1-1+n))))


(defthm d-c2od-c2
  (implies (and (inv-c2 n a)
		(integerp n))
	   (EQUAL (D-C2 (+ N -1) (D-C2 N a))
		  (ZERO-C2 (+ -1 -1 N))))
  :hints (("Goal" :in-theory (disable d-c2-1+n)
	   :use (:instance |+N-1=-1+N|))))


(defthm inverse-c2-lf2+-1+n
  (implies (and (integerp n)
		(inv-d2 (+ n -1) a))
	   (equal (inverse-c2 (+ N -1) (lf2 (+ -1 N) a))
		  (lf2 (+ -1 N) (inverse-d2 (+ N -1) a))))
   :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm +1+n+1=+n+1+1
  (implies (integerp n)
	   (equal (+ 1 N 1) (+ n 1 1)))
  :rule-classes nil)

(defthm +1+n=n+1
  (implies (integerp n)
	   (equal (+ N 1) (+ 1 n)))
  :rule-classes nil)

(defthm lh1+1+n
  (implies (integerp n)
	   (equal (lh1 (+ 1 n) a)
		  (lh1 (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm inv-d1+1+n+1
  (implies (integerp n)
	   (equal (inv-d1 (+ 1 N 1) a)
		  (inv-d1 (+ n 1 1) a)))
  :hints (("Goal" :use (:instance +1+n+1=+n+1+1))))
			  
(defthm inv-lh1-help
  (IMPLIES (AND (INV-D1 N A) (INTEGERP N))
	   (INV-D1 (+ N 1) (LH1 N A)))
  )

(defthm inv-lh1
  (IMPLIES (AND (INV-D1 (+ 1 N) A) (INTEGERP N))
	   (INV-D1 (+ N 2) (LH1 (+ n 1) A)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			(:instance inv-lh1-help (n (+ n 1)))))))


(defthm inverse-d2+1+n
  (implies (integerp n)
	   (equal (inverse-d2 (+ 1 n) a)
		  (inverse-d2 (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm group-operation-inverse-d2+1+n
  (implies (and (inv-d2 (+ N 1) a)
		(inv-d2 (+ N 1) b)
		(integerp n))
	   (equal (INVERSE-d2 (+ 1 N)
                   (GROUP-OPERATION-d2 (+ N 1) a b))
		  (GROUP-OPERATION-d2 (+ N 1)
                           (INVERSE-d2 (+ 1 N)  a)
                           (INVERSE-d2 (+ 1 N) b))))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm inverse-external-d2+1+n
  (implies (and (inv-d2 (+ n 1) a)
		(INV-RING-Z R)
		(integerp n))
	   (EQUAL (INVERSE-D2 (+ 1 N)
                   (EXTERNAL-D2 (+ N 1)
                                R a))
		  (EXTERNAL-D2 (+ N 1)
			       R
			       (INVERSE-D2 (+ 1 N) a))))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm inverse-inverse-d2+1+n
  (implies (and (inv-d2 (+ n 1) a)
		(integerp n))
	   (EQUAL (INVERSE-D2 (+ 1 N)
                   (INVERSE-D2 (+ N 1) a))
		  (INVERSE-D2 (+ N 1)
			      (INVERSE-D2 (+ 1 N) a))))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm |+1-1+N=N|
  (implies (integerp n)
	   (equal (+ 1 -1 N) n)) 
  :rule-classes nil)


(defthm d-d1+1-1+n
  (implies (integerp n)
	   (equal (d-d1 (+ 1 -1 N) a)
		  (d-d1 n a)))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))
			


(defthm d-d1od-d1-help
  (implies (and (inv-d1 n a)
		(integerp n))
	   (EQUAL (D-D1 (1- n) (D-D1 n a))
		  (ZERO-D1 (+ -1 -1 N))))
 )


(defthm |-1-1+1+N=-1+N|
  (implies (integerp n)
	   (equal (+ -1 -1 (+ 1 n))
		  (+ -1 n)))
  :rule-classes nil)


(defthm d-d1od-d1
  (implies (and (inv-d1 (+ 1 n) a)
		(integerp n))
	   (EQUAL (D-D1 n (D-D1 (+ 1 n) a))
		  (ZERO-D1 (+ -1 N))))
  :hints (("Goal" 
	   :use ((:instance |-1+1+N=N|)
		 (:instance |-1-1+1+N=-1+N|)
		 (:instance d-d1od-d1-help (n (+ 1 n)))))))

(defthm group-operation-d1-zero-d1
  (implies (and (inv-d1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-d1 (+ n -1) (zero-d1 (+ -1 n)) a)
		  a))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm lg1-1+n
  (implies (integerp n)
	   (equal (lg1 (+ -1 N) a)
		  (lg1 (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm lf2-1+n
  (implies (integerp n)
	   (equal (lf2 (+ -1 N) a)
		  (lf2 (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm phi-c2-c1-1+n
  (implies (integerp n)
	   (equal (PHI-C2-C1  (+ -1 N) a)
		  (PHI-C2-C1  (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm group-operation-inverse-d1-1+n
  (implies (and (inv-d1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-d1 (+ -1 N) a (inverse-d1 (+ n -1) a))
		  (zero-d1 (+ n -1))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm |+1-1-1+N=N-1|
  (implies (integerp n)
	   (equal (+ 1 -1 (+ -1 n))
		  (+ n -1)))
  :rule-classes nil)

(defthm zero-d1+1-1-1+n
  (implies (integerp n)
	   (equal (ZERO-D1 (+ 1 -1 -1 N))
		  (ZERO-D1 (+ N -1))))
   :hints (("Goal" :use (:instance |+1-1-1+N=N-1|))))

(defthm d-c1+1-1+n
  (implies (integerp n)
	   (equal (d-c1 (+ 1 -1 N) a)
		  (d-c1 n a)))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))



(defthm d-c1od-c1-help
  (implies (and (inv-c1 n a)
		(integerp n))
	   (EQUAL (D-c1 (1- n) (D-c1 n a))
		  (ZERO-c1 (+ -1 -1 N))))
 )



(defthm d-c1od-c1
  (implies (and (inv-c1 (+ 1 n) a)
		(integerp n))
	   (EQUAL (D-c1 n (D-c1 (+ 1 n) a))
		  (ZERO-c1 (+ -1 N))))
  :hints (("Goal" 
	   :use ((:instance |-1+1+N=N|)
		 (:instance |-1-1+1+N=-1+N|)
		 (:instance d-c1od-c1-help (n (+ 1 n)))))))


(defthm group-operation-c1-zero-c1
  (implies (and (inv-c1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-c1 (+ n -1) (zero-c1 (+ -1 n)) a)
		  a))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm group-operation-inverse-c1-1+n
  (implies (and (inv-c1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-c1 (+ -1 N) a (inverse-c1 (+ n -1) a))
		  (zero-c1 (+ n -1))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm zero-c1+1-1-1+n
  (implies (integerp n)
	   (equal (ZERO-c1 (+ 1 -1 -1 N))
		  (ZERO-c1 (+ N -1))))
   :hints (("Goal" :use (:instance |+1-1-1+N=N-1|))))


(defthm lf1-1+1+n
  (implies (integerp n)
	   (equal (lf1 (+ -1 1 N) a)
		  (lf1 n a)))
  :hints (("Goal" :use (:instance |-1+1+N=N|))))


(defthm lf1+1-1+n
  (implies (integerp n)
	   (equal (lf1 (+ 1 -1 N) a)
		  (lf1 n a)))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))


(defthm |+1+N+1=N+2|
  (implies (integerp n)
	   (equal (+ 1 N 1)
		  (+ N 2)))
  :rule-classes nil)



(defthm lh1-group-operation-d1
  (implies (and (inv-d1 (+ 1 N) a)
		(inv-d1 (+ 1 N) b)
		(integerp n))
	   (EQUAL (LH1 (+ N 1)
            (GROUP-OPERATION-D1 (+ 1 N) a b))
	    (GROUP-OPERATION-D1 (+ 1 N 1)
				(LH1 (+ N 1) a)
				(LH1 (+ N 1) b))))
  :hints (("Goal" :in-theory (disable LH1+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+1+N+1=N+2|)))))


(defthm lh1-external-d1
  (implies (and (inv-d1 (+ 1 N) a)
		(INV-RING-Z R)
		(integerp n))
	   (EQUAL (LH1 (+ N 1)
            (external-D1 (+ 1 N) r a))
	    (EXTERNAL-D1 (+ 1 N 1)
                    R (LH1 (+ N 1) a))))
  :hints (("Goal" :in-theory (disable LH1+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+1+N+1=N+2|)))))

(defthm lh1-zero-d1
  (implies (integerp n)
	   (equal (LH1 (+ N 1) (ZERO-D1 (+ 1 N)))
		  (ZERO-D1 (+ 1 N 1))))
   :hints (("Goal" :in-theory (disable LH1+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+1+N+1=N+2|)))))

(defthm lh1-inverse-d1
  (implies (and (inv-d1 (+ 1 N) a)
		(integerp n))
	   (EQUAL (LH1 (+ N 1)
            (inverse-D1 (+ 1 N)  a))
	    (inverse-D1 (+ 1 N 1)
                     (LH1 (+ N 1) a))))
  :hints (("Goal" :in-theory (disable LH1+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+1+N+1=N+2|)))))


(defthm lg1+1+n-1
  (implies (integerp n)
	   (equal (lg1 (+ 1 N -1) a)
		  (lg1 n a)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm lg1+1+-1+n
  (implies (integerp n)
	   (equal (lg1 (+ 1 -1 N) a)
		  (lg1 n a)))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))

(defthm inverse-d2-lg2+-1+n
  (implies (and (integerp n)
		(inv-c2 (+ n -1) a))
	   (equal (inverse-d2 (+ N -1) (lg2 (+ -1 N) a))
		  (lg2 (+ -1 N) (inverse-c2 (+ N -1) a))))
   :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(DEFTHM |-1+N+1=N|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ -1 n 1) N))
  :RULE-CLASSES NIL)


(defthm lh1-1+1+n
  (implies (integerp n)
	   (equal (lh1 (+ -1 N 1) a)
		  (lh1 n a)))
  :hints (("Goal" :use (:instance |-1+N+1=N|))))


(defthm +n+0=n
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ n 0) N))
  :RULE-CLASSES NIL)

(defthm inverse-d2+n+0
  (implies (integerp n)
	   (equal (inverse-d2 (+ n 0) a)
		  (inverse-d2 n a)))
  :hints (("Goal" :use (:instance +n+0=n))))


(defthm lh2-1+n
  (implies (integerp n)
	   (equal (lh2 (+ -1 N) a)
		  (lh2 (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm d-d2+1+n
  (implies (integerp n)
	   (equal (d-d2 (+ 1 N) a)
		  (d-d2 (+ N 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))
			      

(defthm inv-lh2+n-1-help1
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ n 1) (lh2 n a)))
  )

(defthm inv-lh2+n-1-help
  (implies (and (inv-d2 (+ N -1) a)
		(integerp n))
	   (inv-d2 (+ (+ N -1) 1) (lh2 (+ N -1) a)))
   :hints (("Goal" :use (:instance inv-lh2+n-1-help1 (n (+ N -1))))))

(DEFTHM |+N-1+1=N|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ N -1 1) N))
  :RULE-CLASSES NIL)

(defthm inv-lh2+n-1
  (implies (and (inv-d2 (+ N -1) a)
		(integerp n))
	   (inv-d2 n (lh2 (+ N -1) a)))
  :hints (("Goal" :use ((:instance |+N-1+1=N|)
			(:instance inv-lh2+n-1-help)))))



(defthm inv-d-d2+n+1-help1
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ n -1) (d-d2 n a)))
  )

(defthm inv-d-d2+n-1-help
  (implies (and (inv-d2 (+ N 1) a)
		(integerp n))
	   (inv-d2 (+ (+ N 1) -1) (d-d2 (+ N 1) a)))
   :hints (("Goal" :use (:instance inv-d-d2+n+1-help1 (n (+ N 1))))))

(DEFTHM |+N+1-1=N|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ N 1 -1) N))
  :RULE-CLASSES NIL)

(defthm inv-d-d2+n-1
  (implies (and (inv-d2 (+ N 1) a)
		(integerp n))
	   (inv-d2 n (d-d2 (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+N+1-1=N|)
			(:instance inv-d-d2+n-1-help)))))


(defthm inverse-d2-inverse-d2
  (implies (and (inv-d2 n a)
		(integerp n))
	   (equal (inverse-d2 n (inverse-d2 n a))
		  a)))


(defthm reduction-prop-left-help
  (IMPLIES
   (AND (INV-D2 N GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D2 N (lH2 (+ -1 N) (D-D2 N GNRT))
			(D-D2 (+ 1 N) (lH2 N GNRT))
			)
    (GROUP-OPERATION-D2 N GNRT
			(INVERSE-D2 N (lG2 N (lF2 N GNRT))))))
   :hints (("Goal" :in-theory (disable D-D2+1+N LH2-1+N))))



(defthm reduction-prop-left
  (IMPLIES
   (AND (INV-D2 N GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D2 N (D-D2 (+ N 1) (lH2 N GNRT))
			(lH2 (+ N -1) (D-D2 N GNRT)))
    (GROUP-OPERATION-D2 N GNRT
			(INVERSE-D2 N (lG2 N (lF2 N GNRT))))))
   :hints (("Goal" :in-theory (disable D-D2+1+N LH2-1+N)
	    :use ((:instance reduction-prop-left-help)
		  (:instance GROUP-OPERATION-D2-COMMUTATIVITY
				    (a (D-D2 (+ N 1) (lH2 N GNRT)))
				    (b (lH2 (+ N -1) (D-D2 N GNRT))))
		  (:instance |+1+N=N+1|)
		  (:instance |+N-1=-1+N|)))))


(defthm lf1-lh1+1+1+n-help
  (implies (and (inv-d1 n a)
		(integerp n))
	   (EQUAL (LF1 (+ 1 n) (LH1 n a))
		  (ZERO-C1 (+ 1 n)))))



(defthm lf1-lh1+1+1+n
  (implies (and (inv-d1 (+ 1 n) a)
		(integerp n))
	   (EQUAL (LF1 (+ 1 (+ 1 n)) (LH1 (+ n 1) a))
		  (ZERO-C1 (+ 1 (+ 1 n)))))
  :hints (("Goal" 
	    :use ((:instance lf1-lh1+1+1+n-help (n (+ n 1)))
		  (:instance |+1+N=N+1|)
		  ))))

(defthm lf2+1+n
  (implies (integerp n)
	   (equal (lf2 (+ 1 N) a)
		  (lf2 (+ n 1) a)))
   :hints (("Goal" 
	    :use ((:instance |+1+N=N+1|)))))


(defthm lf2-lh2+1+1+n-help
  (implies (and (inv-d2 n a)
		(integerp n))
	   (EQUAL (LF2 (+ n 1) (LH2 n a))
		  (ZERO-C2 (+ 1 n))))
  :hints (("Goal" :in-theory (disable Lf2+1+N)
	    :use ((:instance |+1+N=N+1|)))))


(defthm inverse-c2-zero-c2
  (implies (integerp n)
	   (EQUAL (INVERSE-C2 (+ N 1) (ZERO-C2 (+ 1 N)))
		  (ZERO-C2 (+ 1 N))))
  :hints (("Goal" 
	    :use ((:instance |+1+N=N+1|)))))

(defthm lh1-lg1+1+1+n-help
  (implies (and (inv-c1 (+ 1 N) a)
		(integerp n))
	   (EQUAL (Lh1 (+ n 1) (Lg1 (+ 1 N) a))
		  (ZERO-D1 (+ 1 1 n))))
  :hints (("Goal"
	    :use ((:instance |+1+N=N+1|)))))


(defthm inverse-d2-zero-d2
  (implies (integerp n)
	   (EQUAL (INVERSE-d2 (+ N 1) (ZERO-d2 (+ 1 N)))
		  (ZERO-d2 (+ 1 N))))
  :hints (("Goal" 
	    :use ((:instance |+1+N=N+1|)))))


(defthm lh1-lh1+1+1+n-help
  (implies (and (inv-d1 n a)
		(integerp n))
	   (EQUAL (Lh1 (+ 1 n) (Lh1 n a))
		  (ZERO-D1 (+ 1 1 n))))
  :hints (("Goal" :in-theory (disable LH1+1+N)
	    )))

(defthm lh1-lh1+1+1+n
  (implies (and (inv-d1 (+ 1 N) a)
		(integerp n))
	   (EQUAL (Lh1 (+ n 2) (Lh1 (+ N 1) a))
		  (ZERO-D1 (+ 1 1 1 n))))
  :hints (("Goal"
	    :use ((:instance lh1-lh1+1+1+n-help (n (+ n 1)))
		  (:instance |+1+N=N+1|)
		  (:instance |+1+N=N+1| (n (+ n 1)))
		  (:instance |+1+N=N+1| (n (+ n 1 1)))))))

(defthm lh2+1+n
  (implies (integerp n)
	   (equal (lh2 (+ 1 N) a)
		  (lh2 (+ n 1) a)))
   :hints (("Goal" 
	    :use ((:instance |+1+N=N+1|)))))


(defthm inverse-d2-inverse-d2+n+2
  (implies (and (inv-d2 (+ N 2) a)
		(integerp n))
	   (equal (inverse-d2 (+ N 2) (inverse-d2 (+ N 2) a))
		  a)))


(defthm inv-lh2+n+1-help1
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ N 1) (lh2 n a)))
   :hints (("Goal" :in-theory (disable LH2+1+N)
	    )))

(defthm inv-lh2+n+1-help
  (implies (and (inv-d2 (+ 1 n) a)
		(integerp n))
	   (inv-d2 (+ N 1 1) (lh2 (+ N 1) a)))
   :hints (("Goal" 
	    :use ((:instance inv-lh2+n+1-help1 (n (+ N 1)))
		  (:instance |+1+N=N+1|)
		  ))))

(defthm inv-lh2+n+1
  (implies (and (inv-d2 (+ 1 n) a)
		(integerp n))
	   (inv-d2 (+ N 2) (lh2 (+ N 1) a)))
   :hints (("Goal" :in-theory (disable LH2+1+N)
	    :use ((:instance |+1+N=N+1|)
		  ))))

(defthm inv-lh2+n+1-help2
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ 1 n) (lh2 n a)))
   :hints (("Goal" :in-theory (disable LH2+1+N)
	   :use ((:instance |+1+N=N+1|)
		  ))))


(defthm lh2-lh2+1+1+n-help
  (implies (and (inv-d2 n a)
		(integerp n))
	   (EQUAL (Lh2 (+ n 1) (Lh2 n a))
		  (ZERO-D2 (+ 1 1 n))))
  :hints (("Goal" :in-theory (disable LH2+1+N)
	    :use ((:instance |+1+N=N+1|)
		  ))))


(defthm d-h1+1-1+n
  (implies (integerp n)
	   (equal (d-h1 (+ 1 -1 N) a)
		  (d-h1 n a)))
  :hints (("Goal" 
	    :use ((:instance |+1-1+N=N|)))))


(defthm rf1+-1+n
  (implies (integerp n)
	   (equal (rf1 (+ -1 N) a)
		  (rf1 (+ N -1) a)))
    :hints (("Goal" 
	    :use ((:instance |+N-1=-1+N|)))))

(defthm rg2+-1+n
  (implies (integerp n)
	   (equal (rg2 (+ -1 N) a)
		  (rg2 (+ N -1) a)))
    :hints (("Goal" 
	    :use ((:instance |+N-1=-1+N|)))))



(defthm zero-h1+1-1-1+n
  (implies (integerp n)
	   (equal (ZERO-h1 (+ 1 -1 -1 N))
		  (ZERO-h1 (+ N -1))))
   :hints (("Goal" :use (:instance |+1-1-1+N=N-1|))))

(defthm d-c1+1-1+n
  (implies (integerp n)
	   (equal (d-c1 (+ 1 -1 N) a)
		  (d-c1 n a)))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))



(defthm d-h1od-h1-help
  (implies (and (inv-h1 n a)
		(integerp n))
	   (EQUAL (D-h1 (1- n) (D-h1 n a))
		  (ZERO-h1 (+ -1 -1 N)))))


(defthm d-h1od-h1
  (implies (and (inv-h1 (+ 1 n) a)
		(integerp n))
	   (EQUAL (D-h1 n (D-h1 (+ 1 n) a))
		  (ZERO-h1 (+ -1 N))))
  :hints (("Goal" 
	   :use ((:instance |-1+1+N=N|)
		 (:instance |-1-1+1+N=-1+N|)
		 (:instance d-h1od-h1-help (n (+ 1 n)))))))


(defthm group-operation-h1-zero-h1
  (implies (and (inv-h1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-h1 (+ n -1) (zero-h1 (+ -1 n)) a)
		  a))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm group-operation-inverse-h1-1+n
  (implies (and (inv-h1 (+ n -1) a)
		(integerp n))
	   (equal (group-operation-h1 (+ -1 N) a (inverse-h1 (+ n -1) a))
		  (zero-h1 (+ n -1))))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm d-h2-1+n
  (implies (integerp n)
	   (equal (d-h2 (+ -1 N) a)
		  (d-h2 (+ N -1) a)))
    :hints (("Goal" 
	    :use ((:instance |+N-1=-1+N|)))))




(defthm inverse-h2-inverse-h2+n-2
  (implies (and (inv-h2 (+ N -2) a)
		(integerp n))
	   (equal (inverse-h2 (+ N -2) (inverse-h2 (+ N -2) a))
		  a)))


(defthm inv-d-h2+n+1-help1
  (implies (and (inv-h2 n a)
		(integerp n))
	   (inv-h2 (+ N -1) (d-h2 n a)))
   :hints (("Goal" :in-theory (disable d-H2-1+N)
	    )))

(defthm inv-d-h2+n+1-help
  (implies (and (inv-h2 (+ n -1) a)
		(integerp n))
	   (inv-h2 (+ N -1 -1) (d-h2 (+ N -1) a)))
   :hints (("Goal" 
	    :use ((:instance inv-d-h2+n+1-help1 (n (+ N -1)))
		  (:instance |+1+N=N+1|)
		  ))))

(defthm inv-d-h2+n+1
  (implies (and (inv-h2 (+ n -1) a)
		(integerp n))
	   (inv-h2 (+ N -2) (d-h2 (+ N -1) a)))
   :hints (("Goal" 
	    :use ((:instance inv-d-h2+n+1-help)))))


(defthm d-h2od-h2-help
  (implies (and (inv-h2 n a)
		(integerp n))
	   (EQUAL (D-h2 (+ n -1) (D-h2 n a))
		  (ZERO-h2 (+ -1 -1 N))))
   :hints (("Goal" :in-theory (disable d-H2-1+N)
	    :use (:instance |+N-1=-1+N|))))


(defthm inv-group-operation-h1
  (implies (and (inv-h1 (+ 1 n) a)
		(inv-h1 (+ 1 n) b)
		(integerp n))
	   (inv-h1 (+ 1 n) (group-operation-h1 (+ 1 n) a b))))



(defthm inv-rf1-lg1-phi-lf2-rh2
  (implies (and (inv-d2 n a)
		(integerp n))
   (inv-h1 (+ 1 n) (RF1 (+ 1 N)
                       (LG1 (+ 1 N)
                            (PHI-C2-C1 (+ 1 N)
                                       (LF2 (+ 1 n) (RH2 N a))))))
   )
   :hints (("Goal" :in-theory (disable LF2+1+N)
	    :use (:instance |+1+N=N+1|))))

(defthm inv-rf1-lg1-phi-lf2-rh2-b
  (implies (and (inv-d2 n a)
		(integerp n))
   (inv-h1 (+ 1 n) (RF1 (+ 1 N)
                       (LG1 (+ 1 N)
                            (PHI-C2-C1 (+ 1 N)
                                       (LF2 (+ n 1) (RH2 N a))))))
   )
   :hints (("Goal" :in-theory (disable LF2+1+N)
	    :use (:instance |+1+N=N+1|))))

(defthm group-operation-d2+n+1
  (implies (integerp n)
	   (equal (group-operation-d2 (+ n 1) a b)
		  (group-operation-d2 (+ 1 n) a b)))
   :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm inv-lf2-rh2
  (implies (and (inv-d2 n a)
		(integerp n))
   (inv-c2 (+ 1 n) (LF2 (+ n 1) (RH2 N a)))
   )
   :hints (("Goal" :in-theory (disable LF2+1+N)
	    :use (:instance |+1+N=N+1|))))


(defthm group-operation-d2-lf2
  (implies (and (inv-d2 (+ n 1) a)
		(inv-d2 (+ n 1) b)
		(integerp n))
	   (equal (lf2 (+ N 1) (group-operation-d2 (+ 1 n) a b))
		  (group-operation-c2 (+ 1 n) (lf2 (+ N 1) a)
				      (lf2 (+ N 1) b))))
  :hints (("Goal" :in-theory (disable group-operation-d2+n+1)
	   :use (:instance |+1+N=N+1|))))

(defthm extenal-c2+n+1
  (implies (integerp n)
	   (equal (external-c2 (+ N 1) r a)
		  (external-c2 (+ 1 n) r a)))
  :hints (("Goal" 
	   :use (:instance |+1+N=N+1|))))



(defthm rf1-lg1-phi-zero
  (implies (integerp n)
	   (equal (RF1 (+ 1 N)
                          (LG1 (+ 1 N)
                               (PHI-C2-C1 (+ 1 N)
					  (ZERO-c2 (+ n 1))
                                          )))
		  (ZERO-H1 (+ 1 N))))
   :hints (("Goal" :in-theory (disable LF2+1+N)
	    :use (:instance |+1+N=N+1|))))


(defthm inverse-c2+n+1
  (implies (integerp n)
	   (equal (inverse-c2 (+ N 1) a)
		  (inverse-c2 (+ 1 n) a)))
  :hints (("Goal" 
	   :use (:instance |+1+N=N+1|))))

(defthm rf1+1-1+n
  (implies (integerp n)
	   (equal (rf1 (+ 1 -1 N) a)
		  (rf1 n a)))
   :hints (("Goal" 
	   :use (:instance |+1-1+N=N|))))


(defthm lf2+n+0
  (implies (integerp n)
	   (equal (lf2 (+ N 0) a)
		  (lf2 n a)))
   :hints (("Goal" 
	   :use (:instance |+N+0=N|))))

(defthm phi+1-1+n
  (implies (integerp n)
	   (equal (PHI-C2-C1 (+ 1 -1 N) a)
		  (PHI-C2-C1 n a)))
   :hints (("Goal" 
	   :use (:instance |+1-1+N=N|))))


(defthm group-operation-h1+1-1+n
  (implies (integerp n)
	   (equal (group-operation-h1 (+ 1 -1 N) a b)
		  (group-operation-h1 n a b)))
   :hints (("Goal" 
	   :use (:instance |+1-1+N=N|))))

(defthm inverse-rf2
  (implies (and (inv-d2 (+ N -1) a)
		(integerp n))
	   (equal (inverse-h2 (+ N -1) (rf2 (+ -1 N) a))
		  (rf2 (+ -1 N) (inverse-d2 (+ N -1) a))))
  :hints (("Goal" :in-theory (disable INVERSE-H2+N-1)
	   :use (:instance |+N-1=-1+N|))))


(defthm zero-d1+n+1
  (implies (integerp n)
	   (equal (zero-d1 (+ N 1))
		  (zero-d1 (+ 1 n))))
  :hints (("Goal" 
	   :use (:instance |+1+N=N+1|))))

(defthm group-operation-c1-zero-c1-b
  (implies (and (inv-c1 (+ N -1) a)
		(integerp n))
	   (equal (GROUP-OPERATION-C1 (+ N -1)
				      a
				      (ZERO-C1 (+ -1 N)))
		  a))
  :hints (("Goal" 
	   :use (:instance |+N-1=-1+N|))))

(defthm group-operation-d2-inverse-d2
  (implies (and (inv-d2 (+ 1 N) a)
		(inv-d2 (+ 1 N) b)
		(integerp n))
	   (EQUAL (INVERSE-D2 (+ N 1)
                   (GROUP-OPERATION-D2 (+ 1 N) a b))
       (GROUP-OPERATION-D2 (+ 1 N)
                           (INVERSE-D2 (+ N 1) a)
                           (INVERSE-D2 (+ N 1) b))))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+N=N+1|))))


(defthm group-operation-d1-zero-c1-b+n+1
  (implies (and (inv-d1 (+ N 1) a)
		(integerp n))
	   (equal (GROUP-OPERATION-d1 (+ N 1)
				      a
				      (ZERO-d1 (+ 1 N)))
		  a))
  :hints (("Goal" :in-theory (disable ZERO-D1+N+1)
	   :use (:instance |+1+N=N+1|))))


(defthm group-operation-d1-zero-c1-b+1+n
  (implies (and (inv-d1 (+ N 1) a)
		(integerp n))
	   (equal (GROUP-OPERATION-d1 (+ 1 N)
				      a
				      (ZERO-d1 (+ 1 N)))
		  a))
  :hints (("Goal" :in-theory (disable ZERO-D1+N+1)
	   :use (:instance |+1+N=N+1|))))


(defthm inv-d-d1+1+1+n
  (implies (and (inv-d1 (+ 1 n) a)
		(integerp n))
	   (inv-d1 (+ 1 n) (d-d1 (+ 1 1 n) (lh1 (+ N 1) a))))
   :hints (("Goal" 
	   :use (:instance |+1+N=N+1|))))

(defthm group-operation-d1-zero-c1-b+1+n-bis
  (implies (and (inv-d1 (+ 1 n) a)
		(integerp n))
	   (equal (GROUP-OPERATION-d1 (+ 1 N)
				      (ZERO-d1 (+ 1 N))
				      a
				      )
		  a))
  :hints (("Goal" :in-theory (disable ZERO-D1+N+1)
	   :use (:instance |+1+N=N+1|))))



(defthm reduction-prop-left-help-1
  (IMPLIES
   (AND (INV-D1 N GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D1 N (lH1 (+ -1 N) (D-D1 N GNRT))
			(D-D1 (+ 1 N) (lH1 N GNRT))
			)
    (GROUP-OPERATION-D1 N GNRT
			(INVERSE-D1 N (lG1 N (lF1 N GNRT))))))
   )



(defthm reduction-prop-left-1
  (IMPLIES
   (AND (INV-D1 (+ 1 N)  GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D1 (+ 1 N) (lH1 n (D-D1 (+ 1 N) GNRT))
			(D-D1 (+ 1 1 N) (lH1 (+ N 1) GNRT))
			)
    (GROUP-OPERATION-D1 (+ 1 N) GNRT
			(INVERSE-D1 (+ 1 N) (lG1 (+ 1 N) (lF1 (+ 1 N) GNRT))))))
   :hints (("Goal" :in-theory (disable ZERO-D1+N+1)
	    :use ((:instance reduction-prop-left-help-1 (n (+ 1 N)))
		  (:instance |+1+N=N+1|)
		  (:instance |+N-1=-1+N|)))))


(defthm zero-d2+1+1+n
  (implies (integerp n)
	   (equal (ZERO-D2 (+ 1 1 N))
		  (ZERO-D2 (+ N 2))))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			(:instance |+1+N=N+1| (n (+ n 1)))))))


(defthm zero-h2+1+1+n
  (implies (integerp n)
	   (equal (ZERO-h2 (+ -1 -1 N))
		  (ZERO-h2 (+ N -2))))
  :hints (("Goal" :use ((:instance |+N-1=-1+N| )
			(:instance |+N-1=-1+N| (n (+ n -1)))))))


(defthm rf1+1+n-1
  (implies (integerp n)
	   (equal (rf1 (+ 1 N -1) a)
		  (rf1 n a)))
  :hints (("Goal" :use ((:instance |+N-1=-1+N| )
			))))

(defthm phi+1+n-1
  (implies (integerp n)
	   (equal (PHI-C2-C1 (+ 1 N -1) a)
		  (PHI-C2-C1 n a)))
  :hints (("Goal" :use ((:instance |+N-1=-1+N| )
			))))

(defthm group-operation-d1+n+2
  (implies (integerp n)
	   (equal (group-operation-d1 (+ 1 1 N) a b)
		  (group-operation-d1 (+ N 2) a b)))
   :hints (("Goal" :use ((:instance |+1+N=N+1|)
			(:instance |+1+N=N+1| (n (+ n 1)))))))

(defthm inv-rh1+n+2-help
  (implies (and (inv-d1 n a)
		(integerp n))
	   (inv-d1 (+ n 1) (RH1 n a)))
  :hints (("Goal" :in-theory (disable INV-D1+1+N+1)
	   :use ((:instance |+1+N=N+1|)
		 ))))


(defthm inv-rh1+n+2
  (implies (and (inv-d1 (+ 1 N) a)
		(integerp n))
	   (inv-d1 (+ n 2) (RH1 (+ 1 N) a)))
  :hints (("Goal" :in-theory (disable INV-D1+1+N+1)
	   :use ((:instance inv-rh1+n+2-help (n (+ 1 N)))
		 (:instance |+1+N=N+1| (n (+ n 1)))))))

(defthm inv-rh2+n+1
  (implies (and (inv-d2 n a)
		(integerp n))
	   (inv-d2 (+ 1 n) (rh2 n a)))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))


(defthm zero-c2+n+1
  (implies (integerp n)
	   (equal (ZERO-C2 (+ N 1))
		  (ZERO-C2 (+ 1 N))))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm zero-d1+1+n+1
  (implies (integerp n)
	   (equal (ZERO-d1 (+ 1 N 1))
		  (ZERO-d1 (+ N 2))))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1| (n (+ n 1)))
		 ))))


(defthm inv-rh1-lg1-phi-lf2-rg2
  (implies (and (inv-h2 n a)
		(integerp n))
	   (inv-d1 (+ 1 n) (RH1 N
                           (LG1 N
                                (PHI-C2-C1 N (LF2 N (RG2 N a))))))
	   )
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))


(defthm group-operation-d1+n+1
  (implies (integerp n)
	   (equal (group-operation-d1 (+ n 1) a b)
		  (group-operation-d1 (+ 1 n) a b)))
   :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm external-d1+n+1
  (implies (integerp n)
	   (equal (external-d1 (+ n 1) a b)
		  (external-d1 (+ 1 n) a b)))
   :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))


(defthm inverse-d1+n+1
  (implies (integerp n)
	   (equal (inverse-d1 (+ n 1) a )
		  (inverse-d1 (+ 1 n) a )))
   :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm group-operation-d1+1-1+n
  (implies (integerp n)
	   (equal (group-operation-d1 (+ 1 -1 N) a b)
		  (group-operation-d1 n a b)))
   :hints (("Goal" 
	   :use ((:instance |+N-1=-1+N| )
		 (:instance |+1+N=N+1|)
		 ))))

(defthm inverse-d1+1-1+n
  (implies (integerp n)
	   (equal (inverse-d1 (+ 1 -1 N) a )
		  (inverse-d1 n a )))
   :hints (("Goal" 
	   :use ((:instance |+1-1+N=N|  )
		 
		 ))))

(defthm inverse-d1+1+n-1
  (implies (integerp n)
	   (equal (inverse-d1 (+ 1 n -1) a )
		  (inverse-d1 n a )))
   :hints (("Goal" 
	   :use ((:instance |+1+N-1=N|  )
		 
		 ))))


(defthm rg1+1-1+n
  (implies (integerp n)
	   (equal (rg1 (+ 1 -1 N) a )
		  (rg1 n a )))
   :hints (("Goal" 
	   :use ((:instance |+1-1+N=N|  )
		 
		 ))))

(defthm rg1-1+1+n
  (implies (integerp n)
	   (equal (rg1 (+ -1 +1 N) a )
		  (rg1 n a )))
   :hints (("Goal" 
	   :use ((:instance |-1+1+N=N| )))))

(defthm inverse-d1+n-1
  (implies (integerp n)
	   (equal (inverse-d1 (+ n -1) a )
		  (inverse-d1 (+ -1 n) a )))
   :hints (("Goal" 
	   :use ((:instance |+N-1=-1+N|)
		 ))))


(defthm lf2-zero-d2
  (implies (integerp n)
	   (equal (LF2 (+ N 1) (ZERO-D2 (+ 1 N)))
		  (zero-c2 (+ 1 N))))
  :hints (("Goal" :in-theory (disable ZERO-C2+N+1)
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm rh2+n-1
  (implies (integerp n)
	   (equal (rh2 (+ -1 n) a)
		  (rh2 (+ N -1) a)))
   :hints (("Goal" 
	   :use ((:instance |+N-1=-1+N|)
		 ))))

(defthm inv-rh2-help
  (implies (and (inv-d2 (+ N -1) a)
		(integerp n))
	   (inv-d2 (+ 1 n -1) (rh2 (+ N -1) a)))
  :hints (("Goal" :in-theory (disable RH2+N-1)
	   :use ((:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1| (n (+ N -1)))
		 ))))

(defthm inv-rh2
  (implies (and (inv-d2 (+ N -1) a)
		(integerp n))
	   (inv-d2 n (rh2 (+ N -1) a)))
  :hints (("Goal" :in-theory (disable RH2+N-1)
	   :use ((:instance |+1+N-1=N|)
		 (:instance inv-rh2-help)))))


(defthm reduction-prop-right-help-2
  (IMPLIES
   (AND (INV-D2 N GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D2 N (rH2 (+ -1 N) (D-D2 N GNRT))
			(D-D2 (+ 1 N) (rH2 N GNRT))
			)
    (GROUP-OPERATION-D2 N GNRT
			(INVERSE-D2 N (rG2 N (rF2 N GNRT))))))
   :hints (("Goal" :in-theory (disable RH2+N-1 D-D2+1+N))))



(defthm reduction-prop-right-2
  (IMPLIES
   (AND (INV-D2 N GNRT) (INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-D2 N (D-D2 (+ N 1) (rH2 N GNRT))
			(rH2 (+ N -1) (D-D2 N GNRT)))
    (GROUP-OPERATION-D2 N GNRT
			(INVERSE-D2 N (rG2 N (rF2 N GNRT))))))
   :hints (("Goal" :in-theory (disable RH2+N-1 D-D2+1+N)
	    :use ((:instance reduction-prop-right-help-2 )
		  (:instance group-operation-d2-commutativity (a (rH2 (+ N -1) (D-D2 N GNRT)))
			     (b (D-D2 (+ N 1) (rH2 N GNRT))))
		  (:instance |+1+N=N+1|)
		  (:instance |+N-1=-1+N|)))))


(defthm rf2-inverse-d2
  (implies (and (integerp n)
		(inv-d2 (+ N 1) a))
	   (equal (RF2 (+ 1 N)
		       (INVERSE-D2 (+ N 1) a))
		  (inverse-h2 (+ N 1) (rf2 (+ 1 N) a))))
     :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm inverse-h2+n+1
  (implies (integerp n)
	   (equal (inverse-h2 (+ N 1) a)
		  (inverse-h2 (+ 1 n) a)))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+N=N+1|)
		 ))))

(defthm group-operation-inverse-d1-zero
  (implies (and (inv-d1 (+ N -1) a)
		(integerp n))
	   (equal (group-operation-d1 (+ -1 N) a (inverse-d1 (+ -1 N) a))
		  (zero-d1 (+ N -1))))
:hints (("Goal" :in-theory (disable INVERSE-D1+N-1)
	   :use ((:instance |+N-1=-1+N|)
		 ))))

(defthm rf1-inverse-d1
  (implies (and (integerp n)
		(inv-d1 (+ N -1) a))
	   (equal (RF1 (+ N -1)
		       (INVERSE-D1 (+ -1 n) a))
		  (inverse-h1 (+ N -1) (rf1 (+ N -1) a))))
     :hints (("Goal" :in-theory (disable INVERSE-D1+N-1 GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+N-1=-1+N|)
		 ))))


(defthm group-operation-d1-external-d1+n+2
  (implies (and (inv-d1 (+ N 2) a)
		(inv-d1 (+ N 2) b)
		(INV-RING-Z R)
		(integerp n))
	   (EQUAL (external-D1 (+ 1 N 1) r
                   (GROUP-OPERATION-D1 (+ N 2) a b))
       (GROUP-OPERATION-D1 (+ N 2)
                           (external-D1 (+ 1 N 1) r a)
                           (external-D1 (+ 1 N 1) r b))))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+N+1=N+2|))))


(defthm group-operation-d1-group-operation-d1+n+2
  (implies (and (inv-d1 (+ N 2) a)
		(inv-d1 (+ N 2) b)
		(inv-d1 (+ N 2) c)
		(inv-d1 (+ N 2) d)
		(integerp n))
	   (EQUAL (group-operation-D1 (+ N 2) 
				      (group-operation-d1 (+ 1 N 1) a b)
				      (GROUP-OPERATION-D1 (+ 1 N 1) c d))
		  (group-operation-D1  (+ 1 N 1)
				      (group-operation-d1 (+ N 2) a c)
				      (GROUP-OPERATION-D1 (+ N 2) b d))))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+N+1=N+2|))))


(defthm group-operation-d1-inverse-d1+n+2
  (implies (and (inv-d1 (+ N 2) a)
		(inv-d1 (+ N 2) b)
		(integerp n))
	   (EQUAL (group-operation-D1 (+ N 2) 
				      (inverse-d1 (+ 1 N 1) a)
				      (inverse-D1 (+ 1 N 1) b))
		  (inverse-D1  (+ 1 N 1)
				      (group-operation-d1 (+ N 2) a b)
				      )))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+N+1=N+2|))))


(DEFTHM |+1+1+N=N+2|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ 1 1 N) (+ N 2)))
  :RULE-CLASSES NIL)

(defthm group-operation-d1-rf1+n+2
  (implies (and (inv-d1 (+ N 2) a)
		(inv-d1 (+ N 2) b)
		(integerp n))
	   (EQUAL (rf1  (+ 1 1 n)
			(group-operation-d1 (+ N 2) a b)
			)
		  (group-operation-h1 (+ N 2) 
				      (rf1 (+ 1 1 n) a)
				      (rf1 (+ 1 1 n) b))
		  ))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+1+N=N+2|))))

(defthm zero-h1+1+1+n
  (implies (integerp n)
	   (equal (ZERO-H1 (+ 1 1 N))
		  (ZERO-H1 (+ N 2))))
    :hints (("Goal" 
	   :use (:instance |+1+1+N=N+2|))))


(defthm rh2-inverse-d2
  (implies (and (integerp n)
		(inv-d2 (+ n 1) a))
	   (equal (Rh2 (+ 1 n)
		       (INVERSE-D2 (+ n 1) a))
		  (inverse-d2 (+ N 2) (rh2 (+ 1 n) a))))
     :hints (("Goal" :in-theory (disable INVERSE-H2+N+1 INVERSE-D1+N-1 GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+N=N+1|)
		 ))))


(defthm rf1+lg1-phi-zero-c2
  (implies (integerp n)
	   (equal (RF1 (+ 1 1 N)
		       (LG1 (+ 1 1 N)
			    (PHI-C2-C1 (+ 1 1 N)
				       (ZERO-C2 (+ N 2)))))
		  (ZERO-H1 (+ N 2))))
   :hints (("Goal" :in-theory (disable INVERSE-H2+N+1 INVERSE-D1+N-1 GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+1+N=N+2|)
		 ))))



(defthm group-operation-zero-h1+1+1+n
  (implies (integerp n)
	   (equal (GROUP-OPERATION-H1 (+ 1 1 N) a b)
		  (GROUP-OPERATION-H1 (+ N 2) a b)))
  :hints (("Goal" :in-theory (disable INVERSE-H2+N+1 INVERSE-D1+N-1 GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+1+N=N+2|)
       	 ))))

(defthm zero-d1+1+1+n
  (implies (integerp n)
	   (equal (ZERO-d1 (+ 1 1 N))
		  (ZERO-d1 (+ N 2))))
    :hints (("Goal" 
	   :use (:instance |+1+1+N=N+2|))))

(defthm group-operation-d1-rh1+n+2
  (implies (and (inv-d1 (+ N 2) a)
		(inv-d1 (+ N 2) b)
		(integerp n))
	   (EQUAL (rh1 (+ 1 1 n)
		       (group-operation-d1 (+ N 2) a b)
			)
		  (group-operation-d1 (+ N 3) 
				      (rh1 (+ 1 1 n) a)
				      (rh1 (+ 1 1 n) b))
		  ))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+1+N=N+2|))))


(defthm rh1+lg1-phi-zero-c2
  (implies (integerp n)
	   (equal (Rh1 (+ 1 1 N)
		       (LG1 (+ 1 1 N)
			    (PHI-C2-C1 (+ 1 1 N)
				       (ZERO-C2 (+ N 2)))))
		  (ZERO-d1 (+ N 3))))
   :hints (("Goal" :in-theory (disable INVERSE-H2+N+1 INVERSE-D1+N-1 GROUP-OPERATION-D2+N+1)
	   :use ((:instance |+1+1+N=N+2|)
		 ))))


(defthm zero-d1+1+n+2
  (implies (integerp n)
	   (equal (ZERO-d1 (+ 1 N 2))
		  (ZERO-d1 (+ N 3))))
    :hints (("Goal" 
	   :use (:instance  |+1+N=N+1| (n (+ n 2))))))

(defthm group-operation-d1+1+n+2
  (implies (integerp n)
	   (equal (group-operation-d1 (+ 1 n 2) a b)
		  (group-operation-d1 (+ n 3) a b)))
   :hints (("Goal" 
	   :use (:instance  |+1+N=N+1| (n (+ n 2))))))


(defthm d-c2-lf2+n+1
  (implies (and (inv-d2 (+ N 1) a)
		(integerp n))
	   (EQUAL (d-c2 (+ 1 n) (lf2 (+ n 1) a))
		  (lf2 n (d-d2 (+ 1 n) a))
		  ))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D2+N+1)
	   :use (:instance |+1+N=N+1|))))


(defthm group-operation-d2-distrivutivity-reduction-prop-help1
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n (group-operation-d2 n a b) d)
		  (group-operation-d2 n (group-operation-d2 n c (inverse-d2 n d)) d))
	   ))

(in-theory (disable group-operation-d2-distrivutivity-reduction-prop-help1))


(defthm group-operation-d2-inverse
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(integerp n))
	   (equal (group-operation-d2 n (group-operation-d2 n a (inverse-d2 n b)) b)
		  a))
  :hints (("Goal" :use ((:instance help1 (a a) (b (inverse-d2 n b)) (c b))))))

(defthm group-operation-d2-inverse-bis
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(integerp n))
	   (equal (group-operation-d2 n (group-operation-d2 n a b) (inverse-d2 n b))
		  a))
  :hints (("Goal" :use ((:instance help1 (a a) (b b) (c (inverse-d2 n b)))))))


(defthm group-operation-d2-distrivutivity-reduction-prop-help2
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n (group-operation-d2 n a b) d)
		  c)
	   )
  :hints (("Goal" :in-theory (disable group-operation-d2-distrivutivity-reduction-prop-help1)
	   :use ((:instance group-operation-d2-distrivutivity-reduction-prop-help1)
		 (:instance group-operation-d2-inverse (a c) (b d))))))



(defthm group-operation-d2-group-operation-d2-abc
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(integerp n))
	   (equal (group-operation-d2 n (group-operation-d2 n a b) c)
		  (group-operation-d2 n (group-operation-d2 n c b) a)))
  :hints (("Goal" :use ((:instance help1)
			(:instance group-operation-c2-commutativity (a b) (b c))))))


(defthm group-operation-d2-distrivutivity-reduction-prop-help3
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n (group-operation-d2 n d b) a)
		  c)
	   )
  :hints (("Goal" :in-theory (disable group-operation-d2-distrivutivity-reduction-prop-help1)
	   :use ((:instance group-operation-d2-distrivutivity-reduction-prop-help2)
		 (:instance group-operation-d2-group-operation-d2-abc (c d))))))


(defthm group-operation-d2-distrivutivity-reduction-prop
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n d b)
		  (group-operation-d2 n c (inverse-d2 n a)))
	   )
  :hints (("Goal" :in-theory (disable group-operation-d2-distrivutivity-reduction-prop-help1)
	   :use ((:instance group-operation-d2-distrivutivity-reduction-prop-help3)
		 (:instance group-operation-d2-inverse-bis 
			    (a (group-operation-d2 n d b)) (b a))))))


(defthm rf1-lg1-phi-lf2-group-operation-help1
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(integerp n))
	   (equal (rf1 n (lg1 n (phi-c2-c1 n(lf2 n (group-operation-d2 n a b)))))
		  (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n(lf2 n a))))
				      (rf1 n (lg1 n (phi-c2-c1 n (lf2 n b)))))
		  )))

(in-theory (disable  GROUP-OPERATION-D2-DISTRIVUTIVITY-REDUCTION-PROP))

(defthm rf1-lg1-phi-lf2-group-operation-help2
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(integerp n))
	   (equal (rf1 n (lg1 n (phi-c2-c1 n(lf2 n (group-operation-d2 n a (inverse-d2 n b))))))
		  (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n(lf2 n a))))
				      (inverse-h1 n (rf1 n (lg1 n (phi-c2-c1 n (lf2 n b))))))
		  )))	   



(defthm rf1-lg1-phi-lf2-group-operation
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n(lf2 n a))))
				      (rf1 n (lg1 n (phi-c2-c1 n (lf2 n b)))))
		  (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n (lf2 n c))))
				      (inverse-h1 n (rf1 n (lg1 n (phi-c2-c1 n (lf2 n d))))))))
 :hints (("Goal" :use ((:instance rf1-lg1-phi-lf2-group-operation-help1)
		       (:instance rf1-lg1-phi-lf2-group-operation-help2 (a c) (b d))))) )
		


(defthm reduction-prop-rh2
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D2 N (RH2 (+ N -1) (D-D2 N GNRT))
				(D-D2 (+ N 1) (RH2 N GNRT)))
	    (GROUP-OPERATION-D2 N GNRT
				(INVERSE-D2 N (RG2 N (RF2 N GNRT))))))
  :hints (("Goal" 
	   :use ((:instance  |+1+N=N+1|)
		 (:instance |+N-1=-1+N|)))))


(defthm reduction-prop-rh2-2
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D2 N (RG2 N (RF2 N GNRT))
				(D-D2 (+ N 1) (RH2 N GNRT)))
	    (GROUP-OPERATION-D2 N GNRT
				(INVERSE-D2 N (RH2 (+ N -1) (D-D2 N GNRT))))))
  :hints (("Goal" 
	   :use ((:instance reduction-prop-rh2)
		 (:instance group-operation-d2-distrivutivity-reduction-prop
			    (a (RH2 (+ N -1) (D-D2 N GNRT))) (b (D-D2 (+ N 1) (RH2 N GNRT)))
			    (c GNRT) (d (RG2 N (RF2 N GNRT))))
		 ))))


(defthm rf1-lg1-phi-lf2-group-operation-result
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (equal (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n(lf2 n (RG2 N (RF2 N GNRT))))))
				      (rf1 n (lg1 n (phi-c2-c1 n (lf2 n (D-D2 (+ N 1) (RH2 N GNRT)))))))
		  (group-operation-h1 n
				      (rf1 n (lg1 n (phi-c2-c1 n (lf2 n GNRT))))
				      (inverse-h1 n (rf1 n (lg1 n (phi-c2-c1 n (lf2 n (RH2 (+ N -1) (D-D2 N GNRT))))))))))
 :hints (("Goal" :use ((:instance reduction-prop-rh2-2)
		       (:instance rf1-lg1-phi-lf2-group-operation
				  (a (RG2 N (RF2 N GNRT))) (b (D-D2 (+ N 1) (RH2 N GNRT)))
				  (c GNRT) (d (RH2 (+ N -1) (D-D2 N GNRT))))))) )



(defthm inv-rg1-d-h1
  (implies (and (inv-h1 (+ 1 n) a)
		(integerp n))
	   (inv-d1 n (rg1 n (d-h1 (+ 1 n) a)))))


(defthm upping-d-h2
  (implies (and (inv-h2 n a)
		(integerp n))
	   (equal (rh1 (+ -1 N) (inverse-d1 (+ -1 N) (lg1 (+ N -1) (phi-c2-c1 (+ N -1) (lf2 (+ N -1) (rg2 (+ N -1) (d-h2 n a)))))))
		  (inverse-d1 n (rh1 (+ -1 N) (d-d1 n (lg1 n (phi-c2-c1 n (lf2 n (rg2 n a)))))))))

   :hints (("Goal" :in-theory (disable INVERSE-D1+N-1)
	   :use ((:instance  |+1+N=N+1|)
		 (:instance |+N-1=-1+N|)
		 (:instance |+N+0=N|)))))

(defthm inv-rh1-help
  (implies (and (inv-d1 n a)
		(integerp n))
	   (inv-d1 (+ n 1) (rh1 n a))))
  

(defthm inv-rh1
  (implies (and (inv-d1 (+ -1 N) a)
		(integerp n))
	   (inv-d1 n (rh1 (+ N -1) a)))
  :hints (("Goal" 
	   :use ((:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)
		 (:instance inv-rh1-help (n (+ n -1)))
		 ))))


(defthm inv-rh1-lg1-phi-lf2-rg2-d-h2
  (implies (and (inv-h2 n a)
		(integerp n))
	   (inv-d1 n (rh1 (+ -1 N) (lg1 (+ N -1) (phi-c2-c1 (+ N -1) (lf2 (+ N -1) (rg2 (+ N -1) (d-h2 n a))))))))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N-1)
	   :use ((:instance  |+1+N=N+1|)
		 (:instance |+N-1=-1+N|)
		 ))))

(defthm inverse-inverse-d1
  (implies (and (inv-d1 n a)
		(integerp n))
	   (equal (inverse-d1 n (inverse-d1 n a))
		  a)))


(defthm group-operation-d1-inverse-d1
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(integerp n))
	   (equal (inverse-d1 n (group-operation-d1 n a b))
		  (group-operation-d1 n (inverse-d1 n a) (inverse-d1 n b))))
  :rule-classes nil)



(defthm group-operation-d1-distrivutivity-reduction-prop-help1
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n (inverse-d1 n a) (inverse-d1 n b))
		  (group-operation-d1 n (inverse-d1 n c) d))
	   )
  :hints (("Goal" :use ((:instance group-operation-d1-inverse-d1)
			(:instance group-operation-d1-inverse-d1 (a c) (b (inverse-d1 n d)))))))


(defthm group-opration-d1-zero
  (implies (and (inv-d1 n a)
		(integerp n))
	   (equal (group-operation-d1 n (zero-d1 n) a)
		  a)))

(defthm group-operation-d1-inverse
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(integerp n))
	   (equal (group-operation-d1 n (group-operation-d1 n (inverse-d1 n a) (inverse-d1 n b)) a)
		  (inverse-d1 n b)))
  :hints (("Goal" :use ((:instance group-operation-d1-commutativity (a (inverse-d1 n a)) (b (inverse-d1 n b)))
			(:instance help3 (b (inverse-d1 n a)) (a (inverse-d1 n b)) (c a))
			))))



(defthm group-operation-d1-distrivutivity-reduction-prop-help2
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n (group-operation-d1 n a d) (inverse-d1 n c))
		   (inverse-d1 n b)
		  )
	   )
  :hints (("Goal" 
	   :use ((:instance group-operation-d1-distrivutivity-reduction-prop-help1)
		 (:instance group-operation-d1-inverse)))))

(defthm group-operation-d1-inverse-bis
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(integerp n))
	   (equal (group-operation-d1 n (group-operation-d1 n a (inverse-d1 n b)) b)
		  a))
  :hints (("Goal" :use ((:instance help3 (a a) (c b) (b (inverse-d1 n b)))))))


(defthm group-operation-d1-distrivutivity-reduction-prop-help3
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n (group-operation-d1 n (group-operation-d1 n a d) (inverse-d1 n c)) c)
		  (group-operation-d1 n c (inverse-d1 n b))
		  )
	   )
  :hints (("Goal" 
	   :use ((:instance group-operation-d1-distrivutivity-reduction-prop-help2)
		 ))))




(defthm group-operation-d1-distrivutivity-reduction-prop
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n c (inverse-d1 n b))
		  (group-operation-d1 n d a)
		  )
	   )
  :hints (("Goal"  
	   :use ((:instance group-operation-d1-distrivutivity-reduction-prop-help3)
		 (:instance group-operation-d1-inverse-bis 
			    (a (group-operation-d1 n a d)) (b c))))))



(defthm reduction-prop-rh1-help
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N (RH1 (+ -1 N) (D-D1 N GNRT))
				(D-D1 (+ 1 N) (RH1 N GNRT)))
	    (GROUP-OPERATION-D1 N GNRT
				(INVERSE-D1 N (RG1 N (RF1 N GNRT))))))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N-1)
	   :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)
		 (:instance |+N-1=-1+N|)
		 (:instance  |+1+N=N+1|)
		 ))))


(defthm reduction-prop-rh1
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N (RH1 (+ N -1) (D-D1 N GNRT))
				(D-D1 (+ N 1) (RH1 N GNRT)))
	    (GROUP-OPERATION-D1 N GNRT
				(INVERSE-D1 N (RG1 N (RF1 N GNRT))))))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N-1)
	   :use ((:instance reduction-prop-rh1-help)
		 (:instance |+N-1=-1+N|)
		 (:instance  |+1+N=N+1|)
		 ))))


(defthm inv-d-d1-rh1-help
   (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (inv-d1 (+ (+ n 1) -1) (D-D1 (+ N 1) (RH1 N GNRT))))
  :hints (("Goal" :in-theory (disable ASSOCIATIVITY-OF-+ ))))

(defthm inv-d-d1-rh1
   (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (inv-d1 n (D-D1 (+ N 1) (RH1 N GNRT))))
  :hints (("Goal" :use ((:instance inv-d-d1-rh1-help)
			(:instance |+N+0=N|)
			))))

(defthm reduction-prop-rh1-1
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N gnrt
				(inverse-d1 n (D-D1 (+ 1 n) (RH1 N GNRT)))
				)
	    (GROUP-OPERATION-D1 N (RG1 N (RF1 N GNRT))
				(RH1 (+ -1 n) (D-D1 N GNRT))
				)))
  :hints (("Goal" 
	   :use ((:instance reduction-prop-rh1)
		 (:instance group-operation-d1-distrivutivity-reduction-prop
			    (a (RH1 (+ n -1) (D-D1 N GNRT))) (b (D-D1 (+ n 1) (RH1 N GNRT)))
			    (c GNRT) (d (RG1 N (RF1 N GNRT))))
		 (:instance |+N-1=-1+N|)
		 (:instance  |+1+N=N+1|)))))


(defthm reduction-prop-rh1-result
  (implies (and (inv-h2 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N (lg1 n (phi-c2-c1 n (lf2 n (rg2 n gnrt))))
				(inverse-d1 n (D-D1 (+ 1 n) (RH1 N (lg1 n (phi-c2-c1 n (lf2 n (rg2 n gnrt)))))))
				)
	    (GROUP-OPERATION-D1 N (RG1 N (RF1 N (lg1 n (phi-c2-c1 n (lf2 n (rg2 n gnrt))))))
				(RH1 (+ -1 n) (D-D1 N (lg1 n (phi-c2-c1 n (lf2 n (rg2 n gnrt))))))
				)))
  :hints (("Goal" 
	   :use ((:instance reduction-prop-rh1-1 (gnrt (lg1 n (phi-c2-c1 n (lf2 n (rg2 n gnrt))))))
		 ))))



;;;---------------------------------------------------------------------------

(encapsulate 

 ()

(defthm group-operation-1+n+2
  (implies (integerp n)
	   (equal (group-operation-d1 (+ -1 N 2) a b)
		  (group-operation-d1 (+ 1 n) a b)))
   :hints (("Goal" :in-theory (disable GROUP-OPERATION-D1+N+1)
	   :use ((:instance |+N-1=-1+N|  (n (+ n 2)))
		 (:instance  |+1+N=N+1|)))))


(defthm rh1+1-1+n
  (implies (integerp n)
	   (equal (rh1 (+ 1 -1 N) a)
		  (rh1 n a)))
  :hints (("Goal"
	   :use ((:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1| (n (+ n -1)))
		 (:instance |+N+0=N|)))))


(local 
(defthm prop4-lemma1
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (GROUP-OPERATION-D1
		   (+ 1 N)
		   (CAR GNRT)
		   (GROUP-OPERATION-D1
		    (+ 1 N)
		    (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT))))
		    (GROUP-OPERATION-D1
		     (+ 1 N)
		     (RH1 N
			  (LG1 N
			       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
		     (INVERSE-D1 (+ 1 N)
				 (RG1 (+ 1 N)
				      (RF1 (+ 1 N)
					   (LG1 (+ 1 N)
						(PHI-C2-C1 (+ 1 N)
							   (LF2 (+ N 1)
								(RH2 N (CADR GNRT)))))))))))
		  (group-operation-d1 (+ 1 n)
				    (group-operation-d1 (+ 1 n) (car gnrt)
							(INVERSE-D1 (+ 1 N)
								    (RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT)))))
				    (GROUP-OPERATION-D1
				     (+ 1 N)
				     (RH1 N
					  (LG1 N
					       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
				     (INVERSE-D1 (+ 1 N)
						 (RG1 (+ 1 N)
						      (RF1 (+ 1 N)
							   (LG1 (+ 1 N)
								(PHI-C2-C1 (+ 1 N)
									   (LF2 (+ N 1)
										(RH2 N (CADR GNRT)))))))))))
	   )
:hints (("Goal"
	   :use ((:instance help3 (n (+ 1 N))
			    (a (car gnrt))
			    (b (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT)))))
			    (c (GROUP-OPERATION-D1
				     (+ 1 N)
				     (RH1 N
					  (LG1 N
					       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
				     (INVERSE-D1 (+ 1 N)
						 (RG1 (+ 1 N)
						      (RF1 (+ 1 N)
							   (LG1 (+ 1 N)
								(PHI-C2-C1 (+ 1 N)
									   (LF2 (+ N 1)
										(RH2 N (CADR GNRT)))))))))))
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1| (n (+ n -1))))
)))
)



(local 
(defthm prop4-lemma2-h
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INTEGERP N))
	   (equal (group-operation-d1 (+ 1 n) (car gnrt)
				      (INVERSE-D1 (+ 1 N)
						  (RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT)))))
		  (group-operation-d1 (+ 1 n) (RH1 (+ (+ 1 n) -1) (D-D1 (+ 1 N) (CAR GNRT)))
				      (d-d1 (+ (+ 1 n) 1) (RH1 (+ 1 N) (CAR GNRT))))

		  )
	   )
:hints (("Goal" :use (
		 (:instance reduction-prop-rh1
			    (n (+ 1 n))
			    (gnrt (car gnrt)))
		  ))))
)



(local 


(defthm prop4-lemma2
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INTEGERP N))
	   (equal (group-operation-d1 (+ 1 n) (car gnrt)
				      (INVERSE-D1 (+ 1 N)
						  (RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT)))))
		  (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
				      (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT))))

		  )
	   )
:hints (("Goal" :use (
		 (:instance prop4-lemma2-h)
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1| (n (+ 1 n)))))))
)



(local 

(defthm prop4-lemma3
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (GROUP-OPERATION-D1
		   (+ 1 N)
		   (CAR GNRT)
		   (GROUP-OPERATION-D1
		    (+ 1 N)
		    (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT))))
		    (GROUP-OPERATION-D1
		     (+ 1 N)
		     (RH1 N
			  (LG1 N
			       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
		     (INVERSE-D1 (+ 1 N)
				 (RG1 (+ 1 N)
				      (RF1 (+ 1 N)
					   (LG1 (+ 1 N)
						(PHI-C2-C1 (+ 1 N)
							   (LF2 (+ N 1)
								(RH2 N (CADR GNRT)))))))))))
		  (group-operation-d1 (+ 1 n)
				    (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
				      (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT))))
				    (GROUP-OPERATION-D1
				     (+ 1 N)
				     (RH1 N
					  (LG1 N
					       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
				     (INVERSE-D1 (+ 1 N)
						 (RG1 (+ 1 N)
						      (RF1 (+ 1 N)
							   (LG1 (+ 1 N)
								(PHI-C2-C1 (+ 1 N)
									   (LF2 (+ N 1)
										(RH2 N (CADR GNRT)))))))))))
	   )
:hints (("Goal"
	   :use ((:instance prop4-lemma1)
		 (:instance prop4-lemma2)
		 )
)))
)



(local 


(DEFTHM
  GROUP-OPERATION-D2-INVERSE-D2-b
  (IMPLIES (AND (INV-D2 N A)
		(INV-D2 N B)
		(INTEGERP N))
                           (EQUAL (INVERSE-D2 N (GROUP-OPERATION-D2 N A B))
                                  (GROUP-OPERATION-D2 N (INVERSE-D2 N A)
                                                      (INVERSE-D2 N B))))
                  :RULE-CLASSES NIL)
)



(local 

(defthm group-operation-d2-distrivutivity-reduction-prop-help1-b
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n (inverse-d2 n a) (inverse-d2 n b))
		  (group-operation-d2 n (inverse-d2 n c) d))
	   )
  :hints (("Goal" :use ((:instance group-operation-d2-inverse-d2-b)
			(:instance group-operation-d2-inverse-d2-b (a c) (b (inverse-d2 n d)))))))
)



(local 



(defthm group-operation-d2-inverse-b
  (implies (and (inv-d2 n c)
		(inv-d2 n d)
		(integerp n))
	   (equal (group-operation-d2 n (group-operation-d2 n (inverse-d2 n c) d) c)
		  d))
  :hints (("Goal" :use ((:instance group-operation-d2-commutativity (a (inverse-d2 n c)) (b d))
			(:instance help1 (a d) (b (inverse-d2 n c)) (c c))
			))))
)



(local 



(defthm group-operation-d2-distrivutivity-reduction-prop-help2-b
  (implies (and (inv-d2 n a)
		(inv-d2 n b)
		(inv-d2 n c)
		(inv-d2 n d)
		(integerp n)
		(equal (group-operation-d2 n a b)
		       (group-operation-d2 n c (inverse-d2 n d))))
	   (equal (group-operation-d2 n (group-operation-d2 n (inverse-d2 n a) (inverse-d2 n b))  c)
		   d
		  )
	   )
  :hints (("Goal" 
	   :use ((:instance group-operation-d2-distrivutivity-reduction-prop-help1-b)
		 (:instance group-operation-d2-inverse-b)))))
)



(local 


(defthm reduction-prop-result2
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (group-operation-d2 n
				(GROUP-OPERATION-D2 N (inverse-d2 n (RH2 (+ N -1) (D-D2 N GNRT)))
						    (inverse-d2 n (D-D2 (+ N 1) (RH2 N GNRT))))
				GNRT)
	    (RG2 N (RF2 N GNRT))))
  :hints (("Goal" 
	   :use ((:instance reduction-prop-rh2)
		 (:instance group-operation-d2-distrivutivity-reduction-prop-help2-b
			    (a (RH2 (+ N -1) (D-D2 N GNRT)))
			    (b (D-D2 (+ N 1) (RH2 N GNRT)))
			    (c gnrt)
			    (d (RG2 N (RF2 N GNRT))))
		 ))))
)



(local 



(defthm rh1-lg1-phi-lf2-rg2-rf2=
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (equal (RH1 N
		       (LG1 N
			    (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N gnrt))))))
		  (group-operation-d1 (+ 1 n)
				      (group-operation-d1 (+ 1 n) 
							  (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N GNRT)))))))
							  (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (D-D2 (+ N 1) (RH2 N GNRT))) ))))
							  )
				      (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N gnrt)))))))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N+1
				      GROUP-OPERATION-D1+N+1)
	   :use ((:instance reduction-prop-result2)
			(:instance |+N-1=-1+N|)
			(:instance |+1+N=N+1|)))))

)



(local 




(defthm group-operation-d1-distrivutivity-reduction-prop-help1-b
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n (group-operation-d1 n a b) (inverse-d1 n c))
		  (group-operation-d1 n (group-operation-d1 n c (inverse-d1 n d)) (inverse-d1 n c)))
	   )
:rule-classes nil)

)



(local 



(defthm group-operation-d1-distrivutivity-reduction-prop-help2-b
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(integerp n)
		(equal (group-operation-d1 n a b)
		       (group-operation-d1 n c (inverse-d1 n d))))
	   (equal (group-operation-d1 n (group-operation-d1 n a b) (inverse-d1 n c))
		  (inverse-d1 n d))
	   )
  :hints (("Goal" :in-theory (disable group-operation-d1-distrivutivity-reduction-prop-help1)
	   :use ((:instance group-operation-d1-distrivutivity-reduction-prop-help1-b)
		 (:instance group-operation-d1-inverse (a c) (b d))))))

)



(local 



(defthm reduction-prop-result1
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (group-operation-d1 n
				(GROUP-OPERATION-D1 N (RH1 (+ N -1) (D-D1 N GNRT))
						    (D-D1 (+ N 1) (Rh1 N GNRT)))
				(inverse-d1 n GNRT))
	    (inverse-d1 n (RG1 N (RF1 N GNRT)))))
  :hints (("Goal" :in-theory (disable help3
				      GROUP-OPERATION-D1-DISTRIVUTIVITY)
	   :use ((:instance reduction-prop-rh1)
		 (:instance group-operation-d1-distrivutivity-reduction-prop-help2-b
			    (a (RH1 (+ N -1) (D-D1 N GNRT)))
			    (b (D-D1 (+ N 1) (Rh1 N GNRT)))
			    (c gnrt)
			    (d (RG1 N (RF1 N GNRT))))
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)))))

)



(local 


(defthm reduction-prop-result1-bis
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (group-operation-d1 (+ 1 n)
				(GROUP-OPERATION-D1 (+ 1 n) (RH1 n (D-D1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))
						    (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
				(inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))
	    (inverse-d1 (+ 1 n) (RG1 (+ 1 n) (RF1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))))
  :hints (("Goal" :in-theory (disable  help3 GROUP-OPERATION-D1+N+1 INVERSE-D1+N+1
				      GROUP-OPERATION-D1-DISTRIVUTIVITY)
	   :use ((:instance reduction-prop-result1 (n (+ 1 n))
			    (gnrt (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)
		 (:instance |+1+N-1=N|)))))
)



(local 

(defthm reduction-prop-result1-bis2
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (group-operation-d1 (+ 1 n)
				(GROUP-OPERATION-D1 (+ 1 n) (RH1 n (lg1 n (phi-c2-c1 n (lf2 n (D-D2 (+ n 1) (rh2 n gnrt))))))
						    (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
				(inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))
	    (inverse-d1 (+ 1 n) (RG1 (+ 1 n) (RF1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))))
  :hints (("Goal" :in-theory (disable  help3 GROUP-OPERATION-D1+N+1 INVERSE-D1+N+1
				      GROUP-OPERATION-D1-DISTRIVUTIVITY)
	   :use ((:instance reduction-prop-result1-bis)
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)
		 (:instance |+1+N-1=N|)))))
)



(local 


(defthm eliminate-group-operation-d1-help
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(integerp n))
	   (equal (group-operation-d1 n 
				      (group-operation-d1 n a (inverse-d1 n b)) 
				      (group-operation-d1 n c b))
		  (group-operation-d1 n a c)))
  :hints (("Goal'" :use ((:instance group-operation-d1-commutativity (a c) (b (inverse-d1 n b)))
			 (:instance help3 (a b) (b (INVERSE-D1 N B)) (c c))))))
)



(local 

(defthm eliminate-group-operation-d1
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(inv-d1 n e)
		(integerp n))
	   (equal (group-operation-d1 n 
				      (group-operation-d1 n (group-operation-d1 n a (inverse-d1 n b)) c)
				      (group-operation-d1 n (group-operation-d1 n b d) e))
		  (group-operation-d1 n 
				      (group-operation-d1 n a c)
				      (group-operation-d1 n d e)))

	   )
  :hints (("Goal" :use ((:instance group-operation-d1-commutativity (b (inverse-d1 n b)))
			(:instance help3 (b a) (a (inverse-d1 n b)))
			(:instance group-operation-d1-commutativity (a (inverse-d1 n b))
				   (b (group-operation-d1 n a c)))
			(:instance help3 (a b) (b d) (c e))
			(:instance group-operation-d1-commutativity (a b)
				   (b (group-operation-d1 n d e)))
			(:instance eliminate-group-operation-d1-help
				   (a (group-operation-d1 n a c))
				   (c (group-operation-d1 n d e)))
			)))))



(local 

(defthm inv-inverse-d1-rh1...
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (inv-d1 (+ 1 n) (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N GNRT)))))))))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	   :use ((:instance |+N-1=-1+N|)
			(:instance |+1+N=N+1|))))))



(local 


(defthm inv-rh1-lg1-phi...
    (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (inv-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (D-D2 (+ N 1) (RH2 N GNRT))) )))))
    :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 


(defthm inv-rh1-lg1-phi-lf2
    (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (inv-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N gnrt))))))
    :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 


(defthm d-d1-rh1-lg1...
   (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (inv-d1 (+ 1 n) (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))))
    :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 

(defthm inverse-d1-lg1-phi...
    (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (inv-d1 (+ 1 n) (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
    :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 


(defthm reduction-prop-result-lemma1
  (implies (and (inv-d2 n gnrt)
		(integerp n))
	   (EQUAL
	    (group-operation-d1 (+ 1 n)
				(RH1 N
				     (LG1 N
					  (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N gnrt))))))
				(inverse-d1 (+ 1 n) (RG1 (+ 1 n) (RF1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))))
	    (group-operation-d1 (+ 1 n)
				(group-operation-d1 (+ 1 n) 
						    (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N GNRT)))))))
						    (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N gnrt))))
						    )
				(group-operation-d1 (+ 1 n)
						    (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt))))))
						    (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
				
	    ))
  :hints (("Goal" :in-theory (disable GROUP-OPERATION-D1+N+1 INVERSE-D1+N+1
				      )
	   :use ((:instance rh1-lg1-phi-lf2-rg2-rf2=)
		 (:instance reduction-prop-result1-bis2)
		 (:instance eliminate-group-operation-d1 (n (+ 1 n))
			    (a (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N GNRT))))))))
			    (b (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (D-D2 (+ N 1) (RH2 N GNRT))) ))))
			    (c (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N gnrt)))))
			    (d (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
			    (e (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n gnrt)))))))
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)
		 (:instance |+1+N-1=N|))))))



(local 
(defthm prop4-lemma4
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (GROUP-OPERATION-D1
		   (+ 1 N)
		   (CAR GNRT)
		   (GROUP-OPERATION-D1
		    (+ 1 N)
		    (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT))))
		    (GROUP-OPERATION-D1
		     (+ 1 N)
		     (RH1 N
			  (LG1 N
			       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
		     (INVERSE-D1 (+ 1 N)
				 (RG1 (+ 1 N)
				      (RF1 (+ 1 N)
					   (LG1 (+ 1 N)
						(PHI-C2-C1 (+ 1 N)
							   (LF2 (+ N 1)
								(RH2 N (CADR GNRT)))))))))))
		  (group-operation-d1 (+ 1 n)
				      (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
							  (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT))))
				      (group-operation-d1 (+ 1 n)
							  (group-operation-d1 (+ 1 n) 
									      (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt))))))))
									      (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt)))))
									      )
							  (group-operation-d1 (+ 1 n)
									      (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))
									      (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))))
	   )
:hints (("Goal"
	   :use ((:instance prop4-lemma3)
		 (:instance reduction-prop-result-lemma1 (gnrt (cadr gnrt)))
		 )
))))



(local 
(defthm relocation-group-operation-d1
  (implies (and (inv-d1 n a)
		(inv-d1 n b)
		(inv-d1 n c)
		(inv-d1 n d)
		(inv-d1 n e)
		(inv-d1 n f)
		(integerp n))
	   (equal (group-operation-d1 n 
				      (group-operation-d1 n a b)
				      (group-operation-d1 n 
							  (group-operation-d1 n c d)
							  (group-operation-d1 n e f)))
		  (group-operation-d1 n
				      (group-operation-d1 n 
							  (group-operation-d1 n a d)
							  c)
				      (group-operation-d1 n
							  (group-operation-d1 n  b e)
							  f)
				      )))))



(local 
(defthm inv-d-d1+1+n+1-help
  (implies (and (inv-d1 (+ 1 N) gnrt)
		(integerp n))
	   (inv-d1 (+ (+ (+ 1 N) 1)  -1) (d-d1 (+ (+ 1 N) 1) (RH1 (+ 1 N) gnrt))))
   
:hints (("Goal" :in-theory (disable INVERSE-D1+N+1 ASSOCIATIVITY-OF-+)
	)))     )



(local 
(defthm |+1+N+1-1=+1+N|
  (implies (integerp n)
	   (equal (+ (+ (+ 1 N) 1)  -1)
		  (+ 1 N)))
  :rule-classes nil))



(local 

(defthm inv-d-d1+1+n+1
  (implies (and (inv-d1 (+ 1 N) gnrt)
		(integerp n))
	   (inv-d1 (+ 1 N) (d-d1 (+ 1 1 N) (RH1 (+ 1 N) gnrt))))
   :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance inv-d-d1+1+n+1-help)
		   (:instance |+1+N+1-1=+1+N|)
		   (:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 


(defthm inv-rh1-d-d1+1+n+1-help
  (implies (and (inv-d1 (+ 1 N) gnrt)
		(integerp n))
	   (inv-d1 (+ (+ (+ 1 N) -1) 1) (RH1 (+ (+ 1 N) -1) (D-D1 (+ 1 N) gnrt))))
   :hints (("Goal" :in-theory (disable INVERSE-D1+N+1
				       ASSOCIATIVITY-OF-+)
	     :use ((:instance inv-d-d1+1+n+1-help)
		   (:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 

(defthm |+1+N-1+1=+1+N|
  (implies (integerp n)
	   (equal (+ (+ (+ 1 N) -1)  +1)
		  (+ 1 N)))
  :rule-classes nil))



(local 

(defthm inv-rh1-d-d1+1+n+1
  (implies (and (inv-d1 (+ 1 N) gnrt)
		(integerp n))
	   (inv-d1 (+ 1 N) (RH1 N (D-D1 (+ 1 N) gnrt))))
   :hints (("Goal" :in-theory (disable INVERSE-D1+N+1)
	     :use ((:instance inv-rh1-d-d1+1+n+1-help)
		   (:instance |+1+N-1+1=+1+N|)
		   (:instance |+N-1=-1+N|)
		   (:instance |+1+N=N+1|))))))



(local 


(defthm relocation-lemma
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (group-operation-d1 (+ 1 n)
			       (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
						   (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT))))
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) 
								       (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt))))))))
								       (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt)))))
								       )
						   (group-operation-d1 (+ 1 n)
								       (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))
								       (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))))
	   (group-operation-d1 (+ 1 n)
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
								       (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt))))))
						   (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt)))))))))
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT)))
								       (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
						   (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))
			       )
	   ))
 :hints (("Goal" :in-theory (disable GROUP-OPERATION-D1+N+1 INVERSE-D1+N+1
				      ZERO-D1+N+1)
	   :use ((:instance relocation-group-operation-d1 (n (+ 1 n))
			    (a (RH1 N (D-D1 (+ 1 N) (CAR GNRT))))
			    (b (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT))))
			    (c (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt)))))))))
			    (d (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt))))))
			    (e (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
			    (f (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)
		 (:instance |+1+N-1=N|)))))
)



(local 


(defthm prop4-lemma5
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (GROUP-OPERATION-D1
		   (+ 1 N)
		   (CAR GNRT)
		   (GROUP-OPERATION-D1
		    (+ 1 N)
		    (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT))))
		    (GROUP-OPERATION-D1
		     (+ 1 N)
		     (RH1 N
			  (LG1 N
			       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
		     (INVERSE-D1 (+ 1 N)
				 (RG1 (+ 1 N)
				      (RF1 (+ 1 N)
					   (LG1 (+ 1 N)
						(PHI-C2-C1 (+ 1 N)
							   (LF2 (+ N 1)
								(RH2 N (CADR GNRT)))))))))))
		  (group-operation-d1 (+ 1 n)
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
								       (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt))))))
						   (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt)))))))))
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT)))
								       (D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
						   (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))
			       ))
	   )
:hints (("Goal"
	   :use ((:instance prop4-lemma4)
		 (:instance relocation-lemma)
       	 )
))))



(local 


(defthm group-operation-d1-d-d1
  (implies (and (inv-d1 (+ 1 N 1) a)
		(inv-d1 (+ 1 N 1) b)
		(integerp n))
	   (equal (group-operation-d1 (+ 1 n) (d-d1 (+ 1 N 1) a)
				      (d-d1 (+ 1 N 1) b))
		  (d-d1 (+ 1 N 1) (group-operation-d1 (+ 1 N 1) a b))))
  :hints (("Goal" :use (:instance |+N+0=N|)))))



(local 


(defthm inv-rh1+1+n+1
  (implies (and (inv-d1 (+ N 1) a)
		(integerp n))
	   (inv-d1 (+ 1 (+ N 1)) (rh1 (+ N 1) a)))
  :hints (("Goal" :in-theory (disable INV-D1+1+N+1
				      ASSOCIATIVITY-OF-+)
	   :use ((:instance |+1+N=N+1| (n (+ N 1))))))))



(local 


(defthm prop4-help
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal
	    (group-operation-d1 (+ 1 n) (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT)))
				(D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))) 
	    (d-d1 (+ 1 1 N)
		  (group-operation-d1 (+ 1 1 N)  (RH1 (+ 1 N) (CAR GNRT))
				      (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
	    ))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N+1 ZERO-D1+N+1
				     GROUP-OPERATION-D1+N+1
				     GROUP-OPERATION-D1+N+2)
	   :use ((:instance |+1+N+1-1=+1+N|)
		 (:instance |+N-1=-1+N|)
		 (:instance |+1+N=N+1|))
	   ))))



(local 

(defthm prop4-help-2
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal
	    (group-operation-d1 (+ 1 n) (d-d1 (+ 1 1 N) (RH1 (+ 1 N) (CAR GNRT)))
				(D-D1 (+ (+ 1 n) 1) (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))) 
	    (d-d1 (+ 1 1 N)
		  (group-operation-d1 (+ N 2)  (RH1 (+ 1 N) (CAR GNRT))
				      (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
	    ))
  :hints (("Goal" :in-theory (disable INVERSE-D1+N+1 ZERO-D1+N+1
				     GROUP-OPERATION-D1+N+1
				     )
	   :use ((:instance prop4-help)
		 )
	   ))))



(defthm prop4
  (implies (and (INV-D1 (+ 1 N) (CAR GNRT))
		(INV-D2 N (CADR GNRT))
		(INTEGERP N))
	   (equal (GROUP-OPERATION-D1
		   (+ 1 N)
		   (CAR GNRT)
		   (GROUP-OPERATION-D1
		    (+ 1 N)
		    (INVERSE-D1 (+ 1 N)
				(RG1 (+ 1 N) (RF1 (+ 1 N) (CAR GNRT))))
		    (GROUP-OPERATION-D1
		     (+ 1 N)
		     (RH1 N
			  (LG1 N
			       (PHI-C2-C1 N (LF2 N (RG2 N (RF2 N (CADR GNRT)))))))
		     (INVERSE-D1 (+ 1 N)
				 (RG1 (+ 1 N)
				      (RF1 (+ 1 N)
					   (LG1 (+ 1 N)
						(PHI-C2-C1 (+ 1 N)
							   (LF2 (+ N 1)
								(RH2 N (CADR GNRT)))))))))))
		  (group-operation-d1 (+ 1 n)
			       (group-operation-d1 (+ 1 n)
						   (group-operation-d1 (+ 1 n) (RH1 N (D-D1 (+ 1 N) (CAR GNRT)))
								       (RH1 N (LG1 N (PHI-C2-C1 N (LF2 N (cadr gnrt))))))
						   (inverse-d1 (+ 1 n) (RH1 N (LG1 N (PHI-C2-C1 N (lf2 n (RH2 (+ N -1) (D-D2 N (cadr gnrt)))))))))
			       (group-operation-d1 (+ 1 n)
						   (d-d1 (+ 1 1 N)
						   (group-operation-d1 (+ n 2)  (RH1 (+ 1 N) (CAR GNRT))
								        (Rh1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt))))))))
						   (inverse-d1 (+ 1 n) (lg1 (+ 1 n) (phi-c2-c1 (+ 1 n) (lf2 (+ n 1) (rh2 n (cadr gnrt)))))))
			       ))
	   )
:hints (("Goal" :in-theory (disable INVERSE-D1+N+1 ZERO-D1+N+1
				     GROUP-OPERATION-D1+N+1)
	   :use ((:instance prop4-lemma5)
		 (:instance prop4-help-2))
)))
)




;;;***************************************************************************

(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-cone-cone-d2-d1 'group-suspension-suspension-operation-D1 'zero-cone-cone-d2-d1 
   'external-cone-cone-d2-d1 'inverse-cone-cone-d2-d1 'd-cone-cone-d2-d1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-cone-cone-c2-c1 'group-operation-cone-cone-c2-c1 'zero-cone-cone-c2-c1 'external-cone-cone-c2-c1 'inverse-cone-cone-c2-c1 'd-cone-cone-c2-c1 )
  'lf-cones  'lg-cones  'lh-cones
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-cone-cone-d2-d1 'group-operation-cone-cone-d2-d1 'zero-cone-cone-d2-d1 'external-cone-cone-d2-d1 'inverse-cone-cone-d2-d1 'd-cone-cone-d2-d1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-cone-cone-h2-h1 'group-operation-cone-cone-h2-h1 'zero-cone-cone-h2-h1 'external-cone-cone-h2-h1 'inverse-cone-cone-h2-h1 'd-cone-cone-h2-h1 )
  'rf-cones  'rg-cones  'rh-cones
  ))
'homotopy-equivalence-cones
   )


;;;***************************************************************************


;;;===========================================================================
;;;
;;; End of the proof of the Cone Reduction Theorem (Version 2)
;;;
;;;===========================================================================


;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(phi-d2-d1
   phi-h2-h1
   inv-cone-cone-c2-c1 group-operation-cone-cone-c2-c1 zero-cone-cone-c2-c1 external-cone-cone-c2-c1 inverse-cone-cone-c2-c1 d-cone-cone-c2-c1
   inv-cone-cone-d2-d1 group-operation-cone-cone-d2-d1 zero-cone-cone-d2-d1 external-cone-cone-d2-d1 inverse-cone-cone-d2-d1 d-cone-cone-d2-d1 
   inv-cone-cone-h2-h1 group-operation-cone-cone-h2-h1 zero-cone-cone-h2-h1 external-cone-cone-h2-h1 inverse-cone-cone-h2-h1 d-cone-cone-h2-h1
   lf-cones
   lg-cones
   lh-cones
   rf-cones
   rg-cones
   rh-cones
   |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence|
   )
 )
|#


(defconst *cone-reduction-theorem-v2*
  '((DEFUN PHI-D2-D1 (N A)
        (LG1 N (PHI-C2-C1 N (LF2 N A))))
 (DEFUN PHI-H2-H1 (N A)
        (RF1 N (PHI-D2-D1 N (RG2 N A))))
 (DEFUN INV-CONE-CONE-C2-C1 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-C1 (1+ N) (CAR A))
             (INV-C2 N (CADR A))))
 (DEFUN GROUP-OPERATION-CONE-CONE-C2-C1 (N A B)
        (LIST (GROUP-OPERATION-C1 (1+ N)
                                  (CAR A)
                                  (CAR B))
              (GROUP-OPERATION-C2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-CONE-CONE-C2-C1 (N)
        (LIST (ZERO-C1 (1+ N)) (ZERO-C2 N)))
 (DEFUN EXTERNAL-CONE-CONE-C2-C1 (N A B)
        (LIST (EXTERNAL-C1 (1+ N) A (CAR B))
              (EXTERNAL-C2 N A (CADR B))))
 (DEFUN INVERSE-CONE-CONE-C2-C1 (N A)
        (LIST (INVERSE-C1 (1+ N) (CAR A))
              (INVERSE-C2 N (CADR A))))
 (DEFUN D-CONE-CONE-C2-C1 (N A)
        (LIST (GROUP-OPERATION-C1 N (D-C1 (1+ N) (CAR A))
                                  (PHI-C2-C1 N (CADR A)))
              (INVERSE-C2 (1- N) (D-C2 N (CADR A)))))
 (DEFUN INV-CONE-CONE-D2-D1 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-D1 (1+ N) (CAR A))
             (INV-D2 N (CADR A))))
 (DEFUN GROUP-OPERATION-CONE-CONE-D2-D1 (N A B)
        (LIST (GROUP-OPERATION-D1 (1+ N)
                                  (CAR A)
                                  (CAR B))
              (GROUP-OPERATION-D2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-CONE-CONE-D2-D1 (N)
        (LIST (ZERO-D1 (1+ N)) (ZERO-D2 N)))
 (DEFUN EXTERNAL-CONE-CONE-D2-D1 (N A B)
        (LIST (EXTERNAL-D1 (1+ N) A (CAR B))
              (EXTERNAL-D2 N A (CADR B))))
 (DEFUN INVERSE-CONE-CONE-D2-D1 (N A)
        (LIST (INVERSE-D1 (1+ N) (CAR A))
              (INVERSE-D2 N (CADR A))))
 (DEFUN D-CONE-CONE-D2-D1 (N A)
        (LIST (GROUP-OPERATION-D1 N (D-D1 (1+ N) (CAR A))
                                  (PHI-D2-D1 N (CADR A)))
              (INVERSE-D2 (1- N) (D-D2 N (CADR A)))))
 (DEFUN INV-CONE-CONE-H2-H1 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-H1 (1+ N) (CAR A))
             (INV-H2 N (CADR A))))
 (DEFUN GROUP-OPERATION-CONE-CONE-H2-H1 (N A B)
        (LIST (GROUP-OPERATION-H1 (1+ N)
                                  (CAR A)
                                  (CAR B))
              (GROUP-OPERATION-H2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-CONE-CONE-H2-H1 (N)
        (LIST (ZERO-H1 (1+ N)) (ZERO-H2 N)))
 (DEFUN EXTERNAL-CONE-CONE-H2-H1 (N A B)
        (LIST (EXTERNAL-H1 (1+ N) A (CAR B))
              (EXTERNAL-H2 N A (CADR B))))
 (DEFUN INVERSE-CONE-CONE-H2-H1 (N A)
        (LIST (INVERSE-H1 (1+ N) (CAR A))
              (INVERSE-H2 N (CADR A))))
 (DEFUN D-CONE-CONE-H2-H1 (N A)
        (LIST (GROUP-OPERATION-H1 N (D-H1 (1+ N) (CAR A))
                                  (PHI-H2-H1 N (CADR A)))
              (INVERSE-H2 (1- N) (D-H2 N (CADR A)))))
 (DEFUN LF-CONES (N A)
        (LIST (LF1 (1+ N) (CAR A))
              (LF2 N (CADR A))))
 (DEFUN LG-CONES (N A)
        (LIST (LG1 (1+ N) (CAR A))
              (LG2 N (CADR A))))
 (DEFUN LH-CONES (N A)
        (LIST (LH1 (1+ N) (CAR A))
              (INVERSE-D2 (1+ N) (LH2 N (CADR A)))))
 (DEFUN RF-CONES (N A)
        (LIST (GROUP-OPERATION-H1 (1+ N)
                                  (RF1 (1+ N) (CAR A))
                                  (RF1 (1+ N)
                                       (PHI-D2-D1 (1+ N) (RH2 N (CADR A)))))
              (RF2 N (CADR A))))
 (DEFUN
  RG-CONES (N A)
  (LIST
     (GROUP-OPERATION-D1 (1+ N)
                         (RG1 (1+ N) (CAR A))
                         (INVERSE-D1 (1+ N)
                                     (RH1 N (PHI-D2-D1 N (RG2 N (CADR A))))))
     (RG2 N (CADR A))))
 (DEFUN RH-CONES (N A)
        (LIST (GROUP-OPERATION-D1 (1+ (1+ N))
                                  (RH1 (1+ N) (CAR A))
                                  (RH1 (1+ N)
                                       (PHI-D2-D1 (1+ N) (RH2 N (CADR A)))))
              (INVERSE-D2 (1+ N) (RH2 N (CADR A)))))
 (DEFTHM
  |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence|
  (AND
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-D2-D1 N A)
                 (INV-CONE-CONE-D2-D1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-D2-D1 N
                                 (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INV-CONE-CONE-D2-D1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1
                            N
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-D2-D1
                            N A
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N B C))))
       (INV-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A (ZERO-CONE-CONE-D2-D1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            (ZERO-CONE-CONE-D2-D1 N)))
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-D2-D1 N A (INVERSE-CONE-CONE-D2-D1 N A))
          (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                       (GROUP-OPERATION-CONE-CONE-D2-D1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N R
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-D2-D1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-D2-D1 N S (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
            (GROUP-OPERATION-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)
                                             (INVERSE-CONE-CONE-D2-D1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A))
               (EXTERNAL-CONE-CONE-D2-D1 N S (INVERSE-CONE-CONE-D2-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                       (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N S (ZERO-CONE-CONE-D2-D1 N))
                   (ZERO-CONE-CONE-D2-D1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-D2-D1 (+ N -1)
                                      (D-CONE-CONE-D2-D1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-D2-D1 N A)
                (INV-CONE-CONE-D2-D1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                  (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N -1)
                                                   (D-CONE-CONE-D2-D1 N A)
                                                   (D-CONE-CONE-D2-D1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-D2-D1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                    (EXTERNAL-CONE-CONE-D2-D1 (+ N -1)
                                              R (D-CONE-CONE-D2-D1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                        (ZERO-CONE-CONE-D2-D1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A))
                        (INVERSE-CONE-CONE-D2-D1 (+ N -1)
                                                 (D-CONE-CONE-D2-D1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-D2-D1 (1- N)
                                          (D-CONE-CONE-D2-D1 N A))
                       (ZERO-CONE-CONE-D2-D1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-C2-C1 N A)
                 (INV-CONE-CONE-C2-C1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-C2-C1 N
                                 (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INV-CONE-CONE-C2-C1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1
                            N
                            (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-C2-C1
                            N A
                            (GROUP-OPERATION-CONE-CONE-C2-C1 N B C))))
       (INV-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A (ZERO-CONE-CONE-C2-C1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                            (ZERO-CONE-CONE-C2-C1 N)))
                (EQUAL (INVERSE-CONE-CONE-C2-C1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-C2-C1 N A (INVERSE-CONE-CONE-C2-C1 N A))
          (ZERO-CONE-CONE-C2-C1 N)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                       (GROUP-OPERATION-CONE-CONE-C2-C1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-CONE-CONE-C2-C1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-C2-C1 N R
                                   (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
         (GROUP-OPERATION-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A)
                                          (EXTERNAL-CONE-CONE-C2-C1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-C2-C1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N S A)
                                          (EXTERNAL-CONE-CONE-C2-C1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-C2-C1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-C2-C1 N S (EXTERNAL-CONE-CONE-C2-C1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-C2-C1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-CONE-CONE-C2-C1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-C2-C1 N
                                     (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
            (GROUP-OPERATION-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A)
                                             (INVERSE-CONE-CONE-C2-C1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N S A))
               (EXTERNAL-CONE-CONE-C2-C1 N S (INVERSE-CONE-CONE-C2-C1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
                       (ZERO-CONE-CONE-C2-C1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-C2-C1 N S (ZERO-CONE-CONE-C2-C1 N))
                   (ZERO-CONE-CONE-C2-C1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-C2-C1 (+ N -1)
                                      (D-CONE-CONE-C2-C1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-C2-C1 N A)
                (INV-CONE-CONE-C2-C1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-C2-C1 N
                                     (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
                  (GROUP-OPERATION-CONE-CONE-C2-C1 (+ N -1)
                                                   (D-CONE-CONE-C2-C1 N A)
                                                   (D-CONE-CONE-C2-C1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-C2-C1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A))
                    (EXTERNAL-CONE-CONE-C2-C1 (+ N -1)
                                              R (D-CONE-CONE-C2-C1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
                        (ZERO-CONE-CONE-C2-C1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A))
                        (INVERSE-CONE-CONE-C2-C1 (+ N -1)
                                                 (D-CONE-CONE-C2-C1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-C2-C1 (1- N)
                                          (D-CONE-CONE-C2-C1 N A))
                       (ZERO-CONE-CONE-C2-C1 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INTEGERP N))
                   (INV-CONE-CONE-C2-C1 N (LF-CONES N A)))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INV-CONE-CONE-D2-D1 N B)
                        (INTEGERP N))
                   (EQUAL (LF-CONES N
                                    (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                          (GROUP-OPERATION-CONE-CONE-C2-C1 N (LF-CONES N A)
                                                           (LF-CONES N B))))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (LF-CONES N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                          (EXTERNAL-CONE-CONE-C2-C1 N R (LF-CONES N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (LF-CONES N (ZERO-CONE-CONE-D2-D1 N))
                          (ZERO-CONE-CONE-C2-C1 N)))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INTEGERP N))
                   (EQUAL (LF-CONES N (INVERSE-CONE-CONE-D2-D1 N A))
                          (INVERSE-CONE-CONE-C2-C1 N (LF-CONES N A)))))
     (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                   (INTEGERP N))
              (EQUAL (D-CONE-CONE-C2-C1 N (LF-CONES N A))
                     (LF-CONES (1- N)
                               (D-CONE-CONE-D2-D1 N A)))))
    (AND (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INTEGERP N))
                  (INV-CONE-CONE-D2-D1 (+ N 1)
                                       (LH-CONES N A)))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INV-CONE-CONE-D2-D1 N B)
                       (INTEGERP N))
                  (EQUAL (LH-CONES N
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                         (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N 1)
                                                          (LH-CONES N A)
                                                          (LH-CONES N B))))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INV-RING-Z R)
                       (INTEGERP N))
                  (EQUAL (LH-CONES N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                         (EXTERNAL-CONE-CONE-D2-D1 (+ N 1)
                                                   R (LH-CONES N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (LH-CONES N (ZERO-CONE-CONE-D2-D1 N))
                         (ZERO-CONE-CONE-D2-D1 (+ N 1))))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INTEGERP N))
                  (EQUAL (LH-CONES N (INVERSE-CONE-CONE-D2-D1 N A))
                         (INVERSE-CONE-CONE-D2-D1 (+ N 1)
                                                  (LH-CONES N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-C2-C1 N A)
                 (INV-CONE-CONE-C2-C1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-C2-C1 N
                                 (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INV-CONE-CONE-C2-C1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1
                            N
                            (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-C2-C1
                            N A
                            (GROUP-OPERATION-CONE-CONE-C2-C1 N B C))))
       (INV-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A (ZERO-CONE-CONE-C2-C1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                            (ZERO-CONE-CONE-C2-C1 N)))
                (EQUAL (INVERSE-CONE-CONE-C2-C1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-C2-C1 N A (INVERSE-CONE-CONE-C2-C1 N A))
          (ZERO-CONE-CONE-C2-C1 N)))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INV-CONE-CONE-C2-C1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-C2-C1 N A B)
                       (GROUP-OPERATION-CONE-CONE-C2-C1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-CONE-CONE-C2-C1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-C2-C1 N R
                                   (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
         (GROUP-OPERATION-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A)
                                          (EXTERNAL-CONE-CONE-C2-C1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-C2-C1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N S A)
                                          (EXTERNAL-CONE-CONE-C2-C1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-C2-C1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-C2-C1 N S (EXTERNAL-CONE-CONE-C2-C1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-C2-C1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-CONE-CONE-C2-C1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-C2-C1 N
                                     (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
            (GROUP-OPERATION-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A)
                                             (INVERSE-CONE-CONE-C2-C1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-C2-C1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N S A))
               (EXTERNAL-CONE-CONE-C2-C1 N S (INVERSE-CONE-CONE-C2-C1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
                       (ZERO-CONE-CONE-C2-C1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-C2-C1 N S (ZERO-CONE-CONE-C2-C1 N))
                   (ZERO-CONE-CONE-C2-C1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-C2-C1 (+ N -1)
                                      (D-CONE-CONE-C2-C1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-C2-C1 N A)
                (INV-CONE-CONE-C2-C1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-C2-C1 N
                                     (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
                  (GROUP-OPERATION-CONE-CONE-C2-C1 (+ N -1)
                                                   (D-CONE-CONE-C2-C1 N A)
                                                   (D-CONE-CONE-C2-C1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-C2-C1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-C2-C1 N (EXTERNAL-CONE-CONE-C2-C1 N R A))
                    (EXTERNAL-CONE-CONE-C2-C1 (+ N -1)
                                              R (D-CONE-CONE-C2-C1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-C2-C1 N (ZERO-CONE-CONE-C2-C1 N))
                        (ZERO-CONE-CONE-C2-C1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-C2-C1 N (INVERSE-CONE-CONE-C2-C1 N A))
                        (INVERSE-CONE-CONE-C2-C1 (+ N -1)
                                                 (D-CONE-CONE-C2-C1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-C2-C1 (1- N)
                                          (D-CONE-CONE-C2-C1 N A))
                       (ZERO-CONE-CONE-C2-C1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-D2-D1 N A)
                 (INV-CONE-CONE-D2-D1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-D2-D1 N
                                 (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INV-CONE-CONE-D2-D1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1
                            N
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-D2-D1
                            N A
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N B C))))
       (INV-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A (ZERO-CONE-CONE-D2-D1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            (ZERO-CONE-CONE-D2-D1 N)))
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-D2-D1 N A (INVERSE-CONE-CONE-D2-D1 N A))
          (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                       (GROUP-OPERATION-CONE-CONE-D2-D1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N R
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-D2-D1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-D2-D1 N S (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
            (GROUP-OPERATION-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)
                                             (INVERSE-CONE-CONE-D2-D1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A))
               (EXTERNAL-CONE-CONE-D2-D1 N S (INVERSE-CONE-CONE-D2-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                       (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N S (ZERO-CONE-CONE-D2-D1 N))
                   (ZERO-CONE-CONE-D2-D1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-D2-D1 (+ N -1)
                                      (D-CONE-CONE-D2-D1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-D2-D1 N A)
                (INV-CONE-CONE-D2-D1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                  (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N -1)
                                                   (D-CONE-CONE-D2-D1 N A)
                                                   (D-CONE-CONE-D2-D1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-D2-D1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                    (EXTERNAL-CONE-CONE-D2-D1 (+ N -1)
                                              R (D-CONE-CONE-D2-D1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                        (ZERO-CONE-CONE-D2-D1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A))
                        (INVERSE-CONE-CONE-D2-D1 (+ N -1)
                                                 (D-CONE-CONE-D2-D1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-D2-D1 (1- N)
                                          (D-CONE-CONE-D2-D1 N A))
                       (ZERO-CONE-CONE-D2-D1 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                        (INTEGERP N))
                   (INV-CONE-CONE-D2-D1 N (LG-CONES N A)))
          (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                        (INV-CONE-CONE-C2-C1 N B)
                        (INTEGERP N))
                   (EQUAL (LG-CONES N
                                    (GROUP-OPERATION-CONE-CONE-C2-C1 N A B))
                          (GROUP-OPERATION-CONE-CONE-D2-D1 N (LG-CONES N A)
                                                           (LG-CONES N B))))
          (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (LG-CONES N (EXTERNAL-CONE-CONE-C2-C1 N R A))
                          (EXTERNAL-CONE-CONE-D2-D1 N R (LG-CONES N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (LG-CONES N (ZERO-CONE-CONE-C2-C1 N))
                          (ZERO-CONE-CONE-D2-D1 N)))
          (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                        (INTEGERP N))
                   (EQUAL (LG-CONES N (INVERSE-CONE-CONE-C2-C1 N A))
                          (INVERSE-CONE-CONE-D2-D1 N (LG-CONES N A)))))
     (IMPLIES (AND (INV-CONE-CONE-C2-C1 N A)
                   (INTEGERP N))
              (EQUAL (D-CONE-CONE-D2-D1 N (LG-CONES N A))
                     (LG-CONES (1- N)
                               (D-CONE-CONE-C2-C1 N A)))))
    (IMPLIES (AND (INV-CONE-CONE-C2-C1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-CONES N (LG-CONES N GNRT))
                    GNRT))
    (IMPLIES
     (AND (INV-CONE-CONE-D2-D1 N GNRT)
          (INTEGERP N))
     (EQUAL
      (GROUP-OPERATION-CONE-CONE-D2-D1 N
                                       (LH-CONES (1- N)
                                                 (D-CONE-CONE-D2-D1 N GNRT))
                                       (D-CONE-CONE-D2-D1 (1+ N)
                                                          (LH-CONES N GNRT)))
      (GROUP-OPERATION-CONE-CONE-D2-D1
           N GNRT
           (INVERSE-CONE-CONE-D2-D1 N (LG-CONES N (LF-CONES N GNRT))))))
    (IMPLIES (AND (INV-CONE-CONE-D2-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-CONES (1+ N) (LH-CONES N GNRT))
                    (ZERO-CONE-CONE-C2-C1 (1+ N))))
    (IMPLIES (AND (INV-CONE-CONE-C2-C1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-CONES N (LG-CONES N GNRT))
                    (ZERO-CONE-CONE-D2-D1 (1+ N))))
    (IMPLIES (AND (INV-CONE-CONE-D2-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-CONES (1+ N) (LH-CONES N GNRT))
                    (ZERO-CONE-CONE-D2-D1 (1+ (1+ N))))))
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-D2-D1 N A)
                 (INV-CONE-CONE-D2-D1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-D2-D1 N
                                 (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INV-CONE-CONE-D2-D1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1
                            N
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-D2-D1
                            N A
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N B C))))
       (INV-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A (ZERO-CONE-CONE-D2-D1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            (ZERO-CONE-CONE-D2-D1 N)))
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-D2-D1 N A (INVERSE-CONE-CONE-D2-D1 N A))
          (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                       (GROUP-OPERATION-CONE-CONE-D2-D1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N R
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-D2-D1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-D2-D1 N S (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
            (GROUP-OPERATION-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)
                                             (INVERSE-CONE-CONE-D2-D1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A))
               (EXTERNAL-CONE-CONE-D2-D1 N S (INVERSE-CONE-CONE-D2-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                       (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N S (ZERO-CONE-CONE-D2-D1 N))
                   (ZERO-CONE-CONE-D2-D1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-D2-D1 (+ N -1)
                                      (D-CONE-CONE-D2-D1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-D2-D1 N A)
                (INV-CONE-CONE-D2-D1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                  (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N -1)
                                                   (D-CONE-CONE-D2-D1 N A)
                                                   (D-CONE-CONE-D2-D1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-D2-D1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                    (EXTERNAL-CONE-CONE-D2-D1 (+ N -1)
                                              R (D-CONE-CONE-D2-D1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                        (ZERO-CONE-CONE-D2-D1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A))
                        (INVERSE-CONE-CONE-D2-D1 (+ N -1)
                                                 (D-CONE-CONE-D2-D1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-D2-D1 (1- N)
                                          (D-CONE-CONE-D2-D1 N A))
                       (ZERO-CONE-CONE-D2-D1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-H2-H1 N A)
                 (INV-CONE-CONE-H2-H1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-H2-H1 N
                                 (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INV-CONE-CONE-H2-H1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1
                            N
                            (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-H2-H1
                            N A
                            (GROUP-OPERATION-CONE-CONE-H2-H1 N B C))))
       (INV-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A (ZERO-CONE-CONE-H2-H1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                            (ZERO-CONE-CONE-H2-H1 N)))
                (EQUAL (INVERSE-CONE-CONE-H2-H1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-H2-H1 N A (INVERSE-CONE-CONE-H2-H1 N A))
          (ZERO-CONE-CONE-H2-H1 N)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                       (GROUP-OPERATION-CONE-CONE-H2-H1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-CONE-CONE-H2-H1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-H2-H1 N R
                                   (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
         (GROUP-OPERATION-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A)
                                          (EXTERNAL-CONE-CONE-H2-H1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-H2-H1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N S A)
                                          (EXTERNAL-CONE-CONE-H2-H1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-H2-H1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-H2-H1 N S (EXTERNAL-CONE-CONE-H2-H1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-H2-H1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-CONE-CONE-H2-H1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-H2-H1 N
                                     (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
            (GROUP-OPERATION-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A)
                                             (INVERSE-CONE-CONE-H2-H1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N S A))
               (EXTERNAL-CONE-CONE-H2-H1 N S (INVERSE-CONE-CONE-H2-H1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
                       (ZERO-CONE-CONE-H2-H1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-H2-H1 N S (ZERO-CONE-CONE-H2-H1 N))
                   (ZERO-CONE-CONE-H2-H1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-H2-H1 (+ N -1)
                                      (D-CONE-CONE-H2-H1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-H2-H1 N A)
                (INV-CONE-CONE-H2-H1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-H2-H1 N
                                     (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
                  (GROUP-OPERATION-CONE-CONE-H2-H1 (+ N -1)
                                                   (D-CONE-CONE-H2-H1 N A)
                                                   (D-CONE-CONE-H2-H1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-H2-H1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A))
                    (EXTERNAL-CONE-CONE-H2-H1 (+ N -1)
                                              R (D-CONE-CONE-H2-H1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
                        (ZERO-CONE-CONE-H2-H1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A))
                        (INVERSE-CONE-CONE-H2-H1 (+ N -1)
                                                 (D-CONE-CONE-H2-H1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-H2-H1 (1- N)
                                          (D-CONE-CONE-H2-H1 N A))
                       (ZERO-CONE-CONE-H2-H1 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INTEGERP N))
                   (INV-CONE-CONE-H2-H1 N (RF-CONES N A)))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INV-CONE-CONE-D2-D1 N B)
                        (INTEGERP N))
                   (EQUAL (RF-CONES N
                                    (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                          (GROUP-OPERATION-CONE-CONE-H2-H1 N (RF-CONES N A)
                                                           (RF-CONES N B))))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (RF-CONES N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                          (EXTERNAL-CONE-CONE-H2-H1 N R (RF-CONES N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (RF-CONES N (ZERO-CONE-CONE-D2-D1 N))
                          (ZERO-CONE-CONE-H2-H1 N)))
          (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                        (INTEGERP N))
                   (EQUAL (RF-CONES N (INVERSE-CONE-CONE-D2-D1 N A))
                          (INVERSE-CONE-CONE-H2-H1 N (RF-CONES N A)))))
     (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                   (INTEGERP N))
              (EQUAL (D-CONE-CONE-H2-H1 N (RF-CONES N A))
                     (RF-CONES (1- N)
                               (D-CONE-CONE-D2-D1 N A)))))
    (AND (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INTEGERP N))
                  (INV-CONE-CONE-D2-D1 (+ N 1)
                                       (RH-CONES N A)))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INV-CONE-CONE-D2-D1 N B)
                       (INTEGERP N))
                  (EQUAL (RH-CONES N
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                         (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N 1)
                                                          (RH-CONES N A)
                                                          (RH-CONES N B))))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INV-RING-Z R)
                       (INTEGERP N))
                  (EQUAL (RH-CONES N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                         (EXTERNAL-CONE-CONE-D2-D1 (+ N 1)
                                                   R (RH-CONES N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (RH-CONES N (ZERO-CONE-CONE-D2-D1 N))
                         (ZERO-CONE-CONE-D2-D1 (+ N 1))))
         (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                       (INTEGERP N))
                  (EQUAL (RH-CONES N (INVERSE-CONE-CONE-D2-D1 N A))
                         (INVERSE-CONE-CONE-D2-D1 (+ N 1)
                                                  (RH-CONES N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-H2-H1 N A)
                 (INV-CONE-CONE-H2-H1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-H2-H1 N
                                 (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INV-CONE-CONE-H2-H1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1
                            N
                            (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-H2-H1
                            N A
                            (GROUP-OPERATION-CONE-CONE-H2-H1 N B C))))
       (INV-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A (ZERO-CONE-CONE-H2-H1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                            (ZERO-CONE-CONE-H2-H1 N)))
                (EQUAL (INVERSE-CONE-CONE-H2-H1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-H2-H1 N A (INVERSE-CONE-CONE-H2-H1 N A))
          (ZERO-CONE-CONE-H2-H1 N)))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INV-CONE-CONE-H2-H1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1 N A B)
                       (GROUP-OPERATION-CONE-CONE-H2-H1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-CONE-CONE-H2-H1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-H2-H1 N R
                                   (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
         (GROUP-OPERATION-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A)
                                          (EXTERNAL-CONE-CONE-H2-H1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-H2-H1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N S A)
                                          (EXTERNAL-CONE-CONE-H2-H1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-H2-H1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-H2-H1 N S (EXTERNAL-CONE-CONE-H2-H1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-H2-H1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-CONE-CONE-H2-H1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-H2-H1 N
                                     (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
            (GROUP-OPERATION-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A)
                                             (INVERSE-CONE-CONE-H2-H1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-H2-H1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N S A))
               (EXTERNAL-CONE-CONE-H2-H1 N S (INVERSE-CONE-CONE-H2-H1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
                       (ZERO-CONE-CONE-H2-H1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-H2-H1 N S (ZERO-CONE-CONE-H2-H1 N))
                   (ZERO-CONE-CONE-H2-H1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-H2-H1 (+ N -1)
                                      (D-CONE-CONE-H2-H1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-H2-H1 N A)
                (INV-CONE-CONE-H2-H1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-H2-H1 N
                                     (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
                  (GROUP-OPERATION-CONE-CONE-H2-H1 (+ N -1)
                                                   (D-CONE-CONE-H2-H1 N A)
                                                   (D-CONE-CONE-H2-H1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-H2-H1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-H2-H1 N (EXTERNAL-CONE-CONE-H2-H1 N R A))
                    (EXTERNAL-CONE-CONE-H2-H1 (+ N -1)
                                              R (D-CONE-CONE-H2-H1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-H2-H1 N (ZERO-CONE-CONE-H2-H1 N))
                        (ZERO-CONE-CONE-H2-H1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-H2-H1 N (INVERSE-CONE-CONE-H2-H1 N A))
                        (INVERSE-CONE-CONE-H2-H1 (+ N -1)
                                                 (D-CONE-CONE-H2-H1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-H2-H1 (1- N)
                                          (D-CONE-CONE-H2-H1 N A))
                       (ZERO-CONE-CONE-H2-H1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES
            (AND (INV-CONE-CONE-D2-D1 N A)
                 (INV-CONE-CONE-D2-D1 N B)
                 (INTEGERP N))
            (INV-CONE-CONE-D2-D1 N
                                 (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INV-CONE-CONE-D2-D1 N C)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1
                            N
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            C)
                       (GROUP-OPERATION-CONE-CONE-D2-D1
                            N A
                            (GROUP-OPERATION-CONE-CONE-D2-D1 N B C))))
       (INV-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A (ZERO-CONE-CONE-D2-D1 N))
               A))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (INV-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                            (ZERO-CONE-CONE-D2-D1 N)))
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N A) B))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INTEGERP N))
        (EQUAL
          (GROUP-OPERATION-CONE-CONE-D2-D1 N A (INVERSE-CONE-CONE-D2-D1 N A))
          (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INV-CONE-CONE-D2-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1 N A B)
                       (GROUP-OPERATION-CONE-CONE-D2-D1 N B A)))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N R
                                   (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
         (EXTERNAL-CONE-CONE-D2-D1 N (ADDITION-RING-Z S R)
                                   A)
         (GROUP-OPERATION-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A)
                                          (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL
            (EXTERNAL-CONE-CONE-D2-D1 N (PRODUCT-RING-Z S R)
                                      A)
            (EXTERNAL-CONE-CONE-D2-D1 N S (EXTERNAL-CONE-CONE-D2-D1 N R A))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N (UNIT-Z) A)
                       A))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-CONE-CONE-D2-D1 N B)
             (INTEGERP N))
        (EQUAL
            (INVERSE-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
            (GROUP-OPERATION-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A)
                                             (INVERSE-CONE-CONE-D2-D1 N B))))
       (IMPLIES
        (AND (INV-CONE-CONE-D2-D1 N A)
             (INV-RING-Z S)
             (INTEGERP N))
        (EQUAL (INVERSE-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N S A))
               (EXTERNAL-CONE-CONE-D2-D1 N S (INVERSE-CONE-CONE-D2-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                       (ZERO-CONE-CONE-D2-D1 N)))
       (IMPLIES
            (AND (INV-RING-Z S) (INTEGERP N))
            (EQUAL (EXTERNAL-CONE-CONE-D2-D1 N S (ZERO-CONE-CONE-D2-D1 N))
                   (ZERO-CONE-CONE-D2-D1 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (INV-CONE-CONE-D2-D1 (+ N -1)
                                      (D-CONE-CONE-D2-D1 N A)))
        (IMPLIES
           (AND (INV-CONE-CONE-D2-D1 N A)
                (INV-CONE-CONE-D2-D1 N B)
                (INTEGERP N))
           (EQUAL (D-CONE-CONE-D2-D1 N
                                     (GROUP-OPERATION-CONE-CONE-D2-D1 N A B))
                  (GROUP-OPERATION-CONE-CONE-D2-D1 (+ N -1)
                                                   (D-CONE-CONE-D2-D1 N A)
                                                   (D-CONE-CONE-D2-D1 N B))))
        (IMPLIES
             (AND (INV-CONE-CONE-D2-D1 N A)
                  (INV-RING-Z R)
                  (INTEGERP N))
             (EQUAL (D-CONE-CONE-D2-D1 N (EXTERNAL-CONE-CONE-D2-D1 N R A))
                    (EXTERNAL-CONE-CONE-D2-D1 (+ N -1)
                                              R (D-CONE-CONE-D2-D1 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-CONE-CONE-D2-D1 N (ZERO-CONE-CONE-D2-D1 N))
                        (ZERO-CONE-CONE-D2-D1 (+ N -1))))
        (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                      (INTEGERP N))
                 (EQUAL (D-CONE-CONE-D2-D1 N (INVERSE-CONE-CONE-D2-D1 N A))
                        (INVERSE-CONE-CONE-D2-D1 (+ N -1)
                                                 (D-CONE-CONE-D2-D1 N A)))))
       (IMPLIES (AND (INV-CONE-CONE-D2-D1 N A)
                     (INTEGERP N))
                (EQUAL (D-CONE-CONE-D2-D1 (1- N)
                                          (D-CONE-CONE-D2-D1 N A))
                       (ZERO-CONE-CONE-D2-D1 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                        (INTEGERP N))
                   (INV-CONE-CONE-D2-D1 N (RG-CONES N A)))
          (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                        (INV-CONE-CONE-H2-H1 N B)
                        (INTEGERP N))
                   (EQUAL (RG-CONES N
                                    (GROUP-OPERATION-CONE-CONE-H2-H1 N A B))
                          (GROUP-OPERATION-CONE-CONE-D2-D1 N (RG-CONES N A)
                                                           (RG-CONES N B))))
          (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (RG-CONES N (EXTERNAL-CONE-CONE-H2-H1 N R A))
                          (EXTERNAL-CONE-CONE-D2-D1 N R (RG-CONES N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (RG-CONES N (ZERO-CONE-CONE-H2-H1 N))
                          (ZERO-CONE-CONE-D2-D1 N)))
          (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                        (INTEGERP N))
                   (EQUAL (RG-CONES N (INVERSE-CONE-CONE-H2-H1 N A))
                          (INVERSE-CONE-CONE-D2-D1 N (RG-CONES N A)))))
     (IMPLIES (AND (INV-CONE-CONE-H2-H1 N A)
                   (INTEGERP N))
              (EQUAL (D-CONE-CONE-D2-D1 N (RG-CONES N A))
                     (RG-CONES (1- N)
                               (D-CONE-CONE-H2-H1 N A)))))
    (IMPLIES (AND (INV-CONE-CONE-H2-H1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-CONES N (RG-CONES N GNRT))
                    GNRT))
    (IMPLIES
     (AND (INV-CONE-CONE-D2-D1 N GNRT)
          (INTEGERP N))
     (EQUAL
      (GROUP-OPERATION-CONE-CONE-D2-D1 N
                                       (RH-CONES (1- N)
                                                 (D-CONE-CONE-D2-D1 N GNRT))
                                       (D-CONE-CONE-D2-D1 (1+ N)
                                                          (RH-CONES N GNRT)))
      (GROUP-OPERATION-CONE-CONE-D2-D1
           N GNRT
           (INVERSE-CONE-CONE-D2-D1 N (RG-CONES N (RF-CONES N GNRT))))))
    (IMPLIES (AND (INV-CONE-CONE-D2-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-CONES (1+ N) (RH-CONES N GNRT))
                    (ZERO-CONE-CONE-H2-H1 (1+ N))))
    (IMPLIES (AND (INV-CONE-CONE-H2-H1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-CONES N (RG-CONES N GNRT))
                    (ZERO-CONE-CONE-D2-D1 (1+ N))))
    (IMPLIES (AND (INV-CONE-CONE-D2-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-CONES (1+ N) (RH-CONES N GNRT))
                    (ZERO-CONE-CONE-D2-D1 (1+ (1+ N))))))))))


(make-generic-theory *CONE-REDUCTION-THEOREM-v2*)